Date:   Wed, 3 Oct 2018 17:53:59 +0100
From:   Jiong Wang <jiong.wang@...ronome.com>
To:     Alexei Starovoitov <alexei.starovoitov@...il.com>
Cc:     Edward Cree <ecree@...arflare.com>, ast@...nel.org,
        daniel@...earbox.net, netdev@...r.kernel.org
Subject: Re: [RFC PATCH v2 bpf-next 0/2] verifier liveness simplification

On 03/10/2018 16:59, Alexei Starovoitov wrote:
> On Wed, Oct 03, 2018 at 04:36:31PM +0100, Jiong Wang wrote:
<snip...>
>> Now this hasn't happened. I am still debugging the root cause, but kind of
>> feel
>> "64-bit" attribute propagation is the issue, it seems to me it can't be
>> nicely
>> integrated into the existing register read/write propagation infrastructure.
>
> may be share your patches that modify the liveness propagation?

OK, I will share it after some clean up.

>> For
>> example, for a slightly more complex sequence which is composed of three
>> states:
>>
>> State A
>>   ...
>>   10: r6 = *(u32 *)(r10 - 4)
>>   11: r7 = *(u32 *)(r10 - 8)
>>   12: *(u64 *)(r10 - 16) = r6
>>   13: *(u64 *)(r10 - 24) = r7
>>
>> State B
>>   14: r6 += 1
>>   15: r7 += r6
>>   16: *(u32 *)(r10 - 28) = r7
>>
>> State C
>>   ...
>>   17: r3 += r7
>>   18: r4 = 1
>>   19: *(u64 *)(r10 - 32) = r3
>>   20: *(u64 *)(r10 - 40) = r4
>>
>> State A is parent of state B which is parent of state C.
>>
>> Inside state C, at insn 20, r4 is a 64-bit read/use, so its define at 18 is
>> marked as "64-bit". There is no register source at 18, so "64-bit" attribute
>> propagation is stopped.
>>
>> Then at insn 19, r3 is a 64-bit read/use, so its define at 17 is marked as
>> "64-bit" read/use. Insn 17 has two register sources, r3 and r7, they become
>> "64-bit" now, and their definition should be marked as "64-bit".
>>
>> Now if the definition of r3 or r7 comes from parent state, then the parent
>
> ... the definition of r3 _and_ r7 ...
> both need to propagate up with your algo, right?

Yes, all sources of insn 17, both r3 and r7.

>> state
>> should receive a "REG_LIVE_READ64", this is necessary if later another path
>> reaches state C and triggers prune path, for which case that path should
>> know
>> there is "64-bit" use inside state C on some registers, and should use this
>> information to mark "64-bit" insn.
>>
>> If the definition of r3 or r7 is still inside state C, we need to keep
>> walking
>> up the instruction sequences, and propagate "64-bit" attribute upward until
>> it
>> goes beyond the state C.
>>
>> The above propagation logic is quite different from existing register
>> read/write propagation.
>> For the latter, a write just screen up all following read, and a
>> read would propagate directly to its parent is there is not previous write,
>> no instruction analysis is required.
>
> correct.
> with such algo REG_LIVE_WRITTEN shouldn't be screening the propagation.
>
> I think the patches will discuss the algo.
> Also I think the initial state of 'everything is 32-bit safe'
> and make marks to enforce 64-bit-ness is a dangerous algorithmic choice.

Indeed, and I am actually thinking the same thing ...

> Why not to start at a safer state where everything is 64-bit
> and work backward to find out which ones can be 32-bit?
> That will be safer algo in case there are issues with bit like
> you described in above.

... but I failed to find a algo works on making initial state of
"everything is 64-bit". I haven't figured out a way to check that all use of one
definition are 32-bit on all possible code paths, which looks to me is a must for
one insn marked as 32-bit safe.

Powered by blists - more mailing lists