On Wed, Dec 12, 2018 at 08:58:33PM +0000, Edward Cree wrote: > 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).
what is "last exit" ? Around 'process_bpf_exit' bit of code the verifier doesn't know which state lists are not going to be changed. > Also, why do you clean_live_states() in or after the states_equal() > loop, rather than doing it (in just one place) before it? true. can move the call to the beginning of is_state_visited(). > AIUI, being > in is_state_visited() already implies that all explored states are > DONE, whether any of them match cur_state or not. Unfortunately not. That's exactly the issue with liveness that I want to address with this additional safety check. For subprograms states_equal() checks callsite equivalence. That's what is saving the existing liveness from producing incorrect results. The states in state lists of subprogs are still going to be changed. > 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. refcnt was my initial approach, but it needs to walk parentage chain. Also push/pop_stack needs full walk of all chains too. That is too expensive. What kind of refcnt you had in mind? > Rest of series looks good, have my Ack for patches 1-3. > (Though, maybe use a few more capital letters in your commit messages?) Meaning capitalize first letter of the sentences?
