Re: [PATCH] advsync: Fix litmus tests

[Akira Yokosawa <akiyks@gmail.com>]

On 2017/08/25 18:59:44 -0700, Paul E. McKenney wrote:
> On Sat, Aug 26, 2017 at 09:07:33AM +0900, Akira Yokosawa wrote:
>> >From 65f40cf041aa5506e62c25e4ab9fd63d1d34fdd7 Mon Sep 17 00:00:00 2001
>> From: Akira Yokosawa <akiyks@gmail.com>
>> Date: Sat, 26 Aug 2017 08:48:01 +0900
>> Subject: [PATCH] advsync: Fix litmus tests
>>
>> Adjust litmus-test syntax to be accepted by litmus7.
>>
>> Signed-off-by: Akira Yokosawa <akiyks@gmail.com>
>> ---
>> Hi Paul,
>>
>> This is my attempt to make litmus7 happy.
>> herd7 says:
>>
>> --
>> $ herd7 -conf strong.cfg C-WWC+o+o-data-o+o-addr-o.litmus 
>> Test C-WWC+o+o-data-o+o-addr-o Allowed
>> States 5
>> 1:r1=x; 2:r2=u; x=x;
>> 1:r1=x; 2:r2=x; x=a;
>> 1:r1=x; 2:r2=x; x=x;
>> 1:r1=z; 2:r2=u; x=x;
>> 1:r1=z; 2:r2=z; x=x;
>> Ok
>> Witnesses
>> Positive: 1 Negative: 4
>> Condition exists (1:r1=x /\ 2:r2=x /\ x=x)
>> Observation C-WWC+o+o-data-o+o-addr-o Sometimes 1 4
>> Hash=262fd275af47e8ed4fba69491478bb7d
>> --
>>
>> and
>>
>> --
>> $ herd7 -conf strong.cfg C-WWC+o+o-r+o-addr-o.litmus 
>> Test C-WWC+o+o-r-o+o-addr-o Allowed
>> States 4
>> 1:r1=x; 2:r2=u; x=x;
>> 1:r1=x; 2:r2=x; x=a;
>> 1:r1=z; 2:r2=u; x=x;
>> 1:r1=z; 2:r2=z; x=x;
>> No
>> Witnesses
>> Positive: 0 Negative: 4
>> Condition exists (1:r1=x /\ 2:r2=x /\ x=x)
>> Observation C-WWC+o+o-r-o+o-addr-o Never 0 4
>> Hash=607040ae8eb633fee308b55be24729e1
>> --
>>
>> Do these look reasonable?
> 
> They do, but I failed to push out a change, and thus had to hand-apply
> them with some adjustment.  Could you please double-check them?  For
> ease of repairing any errors, I split this into two commits.

Litmus tests as listings in memorder.tex have indentations of tabs.
For consistency, they should be 2 white spaces.

Other than that, the change looks OK to me.

    Thanks, Akira

> 
> Also, I made the memory-barriers section be its own chapter.  At some
> point I should move the litmus tests as well, but am holding off until
> we get these corrected.
> 
> 							Thanx, Paul
> 
>>      Thanks, Akira
>> --
>>  .../advsync/herd/C-WWC+o+o-data-o+o-addr-o.litmus  | 22 ++++++++++---
>>  .../advsync/herd/C-WWC+o+o-r+o-addr-o.litmus       | 24 ++++++++++----
>>  advsync/memorybarriers.tex                         | 38 +++++++++++++++-------
>>  3 files changed, 62 insertions(+), 22 deletions(-)
>>
[...]