[herd,cat] Fix some problems with the C architecture

[maranget]

This PR fixes two problems:

1. Since PR [herd] Petty optimisation of the Cat interpreter #1855, the polymorphic value V.Empty circulates more. Some primitives were performing set and relation normalisation by themselves, overlooking the cases of empty and universe. We fix this by using the already present and complete normalisation functions as_set and as_rel slightly generalised to handle different error reporting.
2. PR [herd] Split exclusive accesses from the X event set #1889 changed how the relation rmw is computed by defining it in stdlb.cat. The Cat definition of the relation rmw assumes that atomic effects are gathered in the set X, which was not the case of the C semantics. As a result the rmw relation was empty when the read-modify-write instructions are implemented by two (atomic) effects.

[akiyks]

The error is fixed, but I see behavior changes in LKMM litmus tests.

Litmus test:

C add_unless_mb

(*
 * Result: Never
 *
 * This litmus test demonstrates that a successful atomic_add_unless
 * acts as a full memory barrier, ensuring that *x=1 propagates to P1
 * before P1 executes *x=2.
 *)

{
	atomic_t z;
}

P0(int *x, int *y, atomic_t *z)
{
	int r0;

	WRITE_ONCE(*x, 1);
	r0 = atomic_add_unless(z,1,5);
	WRITE_ONCE(*y, 1);
}

P1(int *x, int *y)
{
	int r0;

	r0 = READ_ONCE(*y);
	if (r0 == 1)
		WRITE_ONCE(*x, 2);
}

locations [z;]
exists (1:r0=1 /\ x=1)

Expected output

Test add_unless_mb Allowed
States 2
1:r0=0; [x]=1; [z]=1;
1:r0=1; [x]=2; [z]=1;
No
Witnesses
Positive: 0 Negative: 2
Condition exists (1:r0=1 /\ [x]=1)
Observation add_unless_mb Never 0 2
Time add_unless_mb 0.00
Hash=740ecaca893f828d9079c0c827815245

Output as of fix-some-cat-primitives

Test add_unless_mb Allowed
States 3
1:r0=0; [x]=1; [z]=1;
1:r0=1; [x]=1; [z]=1;
1:r0=1; [x]=2; [z]=1;
Ok
Witnesses
Positive: 1 Negative: 2
Condition exists (1:r0=1 /\ [x]=1)
Observation add_unless_mb Sometimes 1 2
Time add_unless_mb 0.00
Hash=740ecaca893f828d9079c0c827815245

There seems to be lost orderings implied by atomic accesses.

[maranget]

Hi @akiyks. This probably is a consequence of PR #1889. I have a look.

[fsestini]

Is delift({}) expected to work? With this PR, I get the following:

$ dune exec herd7 -- -set-libdir herd/libdir -model repro.cat herd/tests/instructions/AArch64/A01.litmus
File "./repro.cat", line 1, characters 6-16: primitive delift: argument mismatch

where repro.cat is:

empty delift({})

[maranget]

Is delift({}) expected to work? With this PR, I get the following:

Nice catch! Fix on its way. It is likely that V.Empty will not occur un ClassRel context, but robustness commands fixing.

[maranget]

Just pushed a small fix for the ClassRel arguments of primitives. In ambiguous cases, I favored event set and relation.

[maranget]

Commit ba788a2 should fix the add_unless_mb problem.

[maranget]

Unfortunately, the added tests would not have caught the add_unless_mb problem because herd7 generates RMW effects for all the read-modify-write instructions of standard C (i.e. non-lkmm), while atomic_add_unless is implemented by emitting an atomic read and an atomic write.

[akiyks]

Just confirmed this restores expected behavior.
Thanks!

[maranget]

Hi @relokin and @HadrienRenaud. I am leaving next Monday for two weeks. Could we merge this PR that fixes two bugs soon?

[HadrienRenaud]

I can't claim to understand all the details nor consequences of those changes, but overall I don't see why we shouldn't merge it

[maranget]

Thanks @HadrienRenaud. Merging.