On 12/12/18 05:28, Alexei Starovoitov wrote: > introduce REG_LIVE_DONE to check the liveness propagation > and prepare the states for merging > See algorithm description in clean_live_states(). > No difference in tests. > > Signed-off-by: Alexei Starovoitov <a...@kernel.org> This feels a bit magic to me, relying as it does on seeing the state again in is_state_visited() after the last continuation is explored (rather than the marking happening as soon as the last exit is reached). Also, why do you clean_live_states() in or after the states_equal() loop, rather than doing it (in just one place) before it? AIUI, being in is_state_visited() already implies that all explored states are DONE, whether any of them match cur_state or not.
A different way I previously thought of was to have a refcount in verifier states (at the time we had a single parent rather than per- register parents) counting live children, that falls to 0 when all continuations have been walked. That was something I did in my bounded loops RFC. With something like that, we could check refcount != 0 in mark_reg_read and check refcount == 0 in explored states in is_state_visited. Seems to me like that gets you the same thing and also adds the guarantee that our explored_states really are fully explored. Rest of series looks good, have my Ack for patches 1-3. (Though, maybe use a few more capital letters in your commit messages?) -Ed
