cache consistency: one has to check whether for each variable, the actions of all threads on that variable can be brought into a sequential order

Causal consistency is PRAM consistency computed with the transitive hull of the usual relation induced by the threads.

GDO consistency

GPO+GDO+GWO consistency

GPO+GDO consistency

GPO+GWO consistency

GPO consistency

GWO consistency

PRAM consistency: one has to check whether for each thread, the writes of all threads plus all actions of the considered thread can be sequentialized

Sequential consistency demands that all actions can be ordered into a single thread such that all WR-constraints are respected and that all actions of each thread are kept in order. To this end, the following function tries to topologically sort the thereby defined partial order.

slow consistency: one has to check whether for each thread and each variable, the writes of all threads on that variable plus all actions on that variable of the considered thread can be brought into a sequential order

check Steinke-Nutt definition for restricted relations relX

the cgi program

compute Steinke-Nutt data order relation; it is the least relation relD with (1) relP is a subset of relD (2) relR is a subset of relD (3) rw(x,v1) <=P read(x,v2) >=R write(x,v2) with v1!=v2 implies rw(x,v1)<=D write(x,v2) (4) relD is transitive

compute Steinke-Nutt write-read-write relation

construct the successor relations of the threads and the WR constraints

compute the set of actions of thread with name tname

compute the set of actions on variable x

compute the set of all write actions

compute the restriction of a relation on a set of actions

Function sequentialize aims at scheduling the given actions into a sequence that is consistent with the partial order relation rel, the WR-constraints, and that is read-write consistent (i.e. read actions read the latest written value). To this end, mem represents the current state of the main memory, so that only read actions can be scheduled that read a value that is currently in the memory. "blocked" is a set of pairs (x,l) that are added whenever a write action is scheduled with a WR-constraint to a read with label l. This means that no write operations writing to variable x can be scheduled until the read with label l has been scheduled (which unblocks the pair (x,l)). "rel" is the partial order relation imposed by the reduced threads and their WR-constraints, and constrWR are the WR-constraints. The sequentialization works as follows: We first compute the set of actions that do not have a predecessor action in rel (otherwise the predecessor must be scheduled first). We then remove all read actions that are not consistent with the current content of the main memory, since these can obviously not scheduled at this stage. Moreover, we remove all write actions that write to a variable x that contains a pair (x,l) in blocked. The remaining actions can all be scheduled, so that we can select any one of these. We may prefer read operations, since these may unblock write actions, and may no longer be scheduled if a write in chosen instead, however, for completeness, we should try all possibilities.