Re: [RFC] tools/memory-model: Rule out OOTA

On 7/24/2025 4:14 PM, Paul E. McKenney wrote:
> On Wed, Jul 23, 2025 at 09:39:05AM -0700, Paul E. McKenney wrote:
>> On Wed, Jul 23, 2025 at 09:26:32AM +0200, Hernan Ponce de Leon wrote:
>>> On 7/23/2025 2:43 AM, Paul E. McKenney wrote:
>>>> On Mon, Jan 06, 2025 at 10:40:03PM +0100, Jonas Oberhauser wrote:
>>>>> The current LKMM allows out-of-thin-air (OOTA), as evidenced in the following
>>>>> example shared on this list a few years ago:
>>>>
>>>> Apologies for being slow, but I have finally added the litmus tests in
>>>> this email thread to the https://github.com/paulmckrcu/litmus repo.
>>>
>>> I do not understand some of the comments in the preamble of the tests:
>>>
>>> (*
>>>   * Result: Never
>>>   *
>>>   * But Sometimes in LKMM as of early 2025, given that 42 is a possible
>>>   * value for things like S19..
>>>   *
>>>   * https://lore.kernel.org/all/[email protected]/
>>>   *)
>>>
>>> I see that herd7 reports one of the states to be [b]=S16. Is this supposed
>>> to be some kind of symbolic state (i.e., any value is possible)?
>>
>> Exactly!
>>
>>> The value in the "Result" is what we would like the model to say if we would
>>> have a perfect version of dependencies, right?
>>
>> In this case, yes.
> 
> I should hasten to add that, compiler optimizations being what they are,
> "perfect" may or may not be attainable, and even if attainable, might
> not be maintainable.

Yes, I just wanted to clarify if this is what herd7 + the current model 
are saying or what developers should expect.

Hernan

> 
> I am pretty sure that you all already understood that, but I felt the
> need to make it explicit.  ;-)
> 
> 							Thanx, Paul