Modeling of Architectures

Abstract

Concurrent programming is known to be quite hard. It is made even harder by the fact that, very often, the execution models of the machines we run our software on are not precisely defined.

This document is a tutorial on the herd tool and the cat language, in which one can define consistency models.

Appendices

A Answers to Exercises

1.1 A.1 First Step in Herding Cats

Exercise: what do you think?. Do you think such an execution is possible?

Yes! On IBM Power or ARM machines for example [5].

1.2 A.2 First Big Cat: Tiger

Exercise: SC per Location with Load-Load Hazard. Certain architectures, such as Sparc RMO [11] allow what is sometimes called load-load hazard, i.e. a situation where the coRR test that we’ve just seen is allowed to yield the result 0:r1=1; 0:r2=0;. How do you think we can build a check that forbids all tests coWW, coRW1, coRW2 and coWR, but allows the test coRR?

In cat speak:

Intuitively what we’re doing here is removing the read-read pairs (R*R) from po-loc to build the po-loc-llh relation, then enforcing that this new relation is compatible with the communication relations com.

Let’s run herd on coWW, coRW1, coRW2, and coWR, and observe that they are still forbidden. Now let’s run it on coRR and observe that it is allowed. We’ve built a check that enforces SC per location but allows for load-load hazards!

Exercise: Implementing Address Dependencies. How do you think we can implement address dependencies? By this I mean that I’d like to see a sequence of instructions which, placed between two reads, implement e.g. an address dependency.

Consider the following variant of MP; the reading thread P1 has an address dependency between its two reads:

This dependency, in conjunction with the lightweight fence on P0, should be enough to forbid the non-SC execution of MP.

Exercise: Distributed. 2+2w Consider the following litmus test, which is essentially a distributed variant of 2+2w:

Which fences should we use to forbid the final state? Why? Where should we put them?

We should put a lightweight fence between the read-write pair on P1, and a lightweight fence between the write-write pair on P2, like so:

This is because the A-cumulativity of the lightweight fence on P1 will impose an ordering between the write of x on P0 and the write of y on P1.

Exercise: Independent Reads of Independent Writes. Consider the following litmus test, known as IRIW:

Which fences should we use to forbid the final state? Why? Where should we put them?

We should put a heavyweight fence between the read-read pairs on P1 and P3, like so:

This is because IRIW essentially is a distributed variant of the store buffering example, therefore reacts to fences in much the same way as SB, just like ISA2 or WRC react to fences (lightweight in their case) in much the same way as MP.

Thus the A-cumulativity of the heavyweight fence will impose an ordering between the write of x on P0 and the read of y on P1 (idem for the write of y on P2 and the read of x on P3).

Exercise: SC and TSO Re-Make Re-Model [9]. Remember that we’ve defined SC and (not quite) TSO earlier. Try to reformulate both models in terms of the five principles we’ve just learnt: sc per location, no thin air, propagation, observation and restoring sc. The SC model you’ll end up with will be equivalent to the one above. The TSO model you’ll end up with will be TSO proper!

Take the tiger cat file, and use the following bell files. For SC:

and for TSO:

1.3 A.3 Second Big Cat: Jaguar

Exercise: Difference Between RMO and Power or ARM What’s a test that distinguishes RMO from Power or ARM (as we’ve defined them previously)? More precisely, what’s a test that’s forbidden on RMO but allowed on Power or ARM?

IRIW+deps distinguishes RMO from Power or ARM:

because it is forbidden on RMO [1, 2], but allowed on Power and ARM [5].

Exercise: Implementing Scope Inclusion. How would you implement an RMO per scope model as above, but where the fences have an effect not only at their scopes, but also at narrower scopes? That is, the fence for system also has an effect at gpu and cta level for example? This procedure should forbid mp-mit-scopes+fgpu+fsys, but not mp-mit-scopes+fcta+fgpu.

We need to invent a recursive notion of wider, that will return, given a scope level s, all scope levels wider than s, not just the immediately wider one:

We can then use this new notion in the way we define our rmo-fences:

Note how we replace the call to tag2events by a call to wider2 in the definition of rmo-fences.

Exercise: Release Sequence. In C++ there’s a notion of release sequence, which says that synchronisation does not just happen via special-rf, i.e. from the special write of a special read-from to the corresponding special read. Rather, it can happen from any write of the same location and on the same thread that precedes (in program order) a special write.

How would you modify our model to include this notion?

Like so (where ? means zero or one step):

B Complete Bell and Cat Files

1.1 B.1 Kittens

Here’s kittens.bell :

Here’s kittens.cat :

1.2 B.2 Tiger

Here’s tiger.bell :

Here’s tiger.cat :

1.3 B.3 Jaguar

Here’s jaguar.bell :

Here’s jaguar.cat :

1.4 B.4 Panther

Here’s panther.bell :

Here’s panther.cat :