Assume you have a sequential operator "seq," a parallel operator "par," and a predicate on programs "valid." Then the following laws hold:

1. If ((a `seq` b) `par` (c `seq` d)) is a valid trace, ((a `par` c) `seq` (b `par` d)) is a valid trace:

  valid ((a `seq` b) `par` (c `seq` d)) -> valid ((a `par` c) `seq` (b `par` d)).

(The first law describes how the execution of several threads can interleave the steps.)

2. Implications may be applied inside other constructs:
  (valid a -> valid b) -> valid (a `seq` c) -> valid (b `seq` c)
  (valid a -> valid b) -> valid (c `seq` a) -> valid (c `seq` b)
  (valid a -> valid b) -> valid (a `par` c) -> valid (b `par` c).

3. Introduction of the identity program:
  valid a <-> valid (a `seq` id)
  valid a <-> valid (id `seq` a)
  valid a <-> valid (a `par` id)
  valid a <-> valid (id `par` a).

4. Define an "elementary program" to be one without any appearances of the seq and par operators. Say you have a program p consisting of a list of elementary programs (a `seq` b `seq` c ...), one distinguished elementary program q, and an arbitrary program r. Then if every way of splitting p into two program sequences p1 and p2 results in the following formula being valid:

  p1 `seq` q `seq` (p2 `par` r)

then it follows that

  p `par` (q `seq` r)

is valid.

(Rule 4 is the opposite of rule 1. Rule 1 allows you to deduce traces from a particular parallel form. Rule 4 allows you to deduce a particular parallel form from a set of traces.)

5. In order to prove a property on an arbitrary program, it is sufficient to prove it on an arbitrary sequence of elementary programs (p1 `seq` p2 `seq` p3 ...). In other words, every program amounts to a set of traces.

6. Associativity of seq:

  valid (p1 `seq` (p2 `seq` p3)) <-> valid ((p1 `seq` p2) `seq` p3).

Someone would use this formalism by first declaring a particular program they are interested in, valid, then following the implications of the validity of that trace, for the validity of other traces.

'''Example proof:'''

The commutativity of "par": valid (a `par` b) -> valid (b `par` a). Proof is by induction on the traces of a.

Base case:
  forall b. valid (id `par` b) -> valid (b `par` id) 
which is obvious.

Inductive step: we start with the original goal, and assume (valid ((x `seq` a) `par` b)) where x is an elementary program.
Now we split b into sequences b1 and b2. For each way of splitting b we get
  valid ((x `seq` a) `par` (b1 `seq` b2))
which implies
  valid (b1 `seq` x `seq` (a `par` b2))
by rule 1. Then we apply the inductive hypothesis to get
  valid (b1 `seq` x `seq` (b2 `par` a)).
Note that all the ways of splitting b correspond to the required hypotheses of rule 4. Therefore we conclude,
  valid (b `par` (x `seq` a))
as required.

'''A useful fact about Hoare clauses and concurrency:'''

Say you have elementary programs a1, a2, a3, a4, ... and elementary programs b1, b2, b3, b4, .... Assume b1, b2, b3, b4 ... are predicate preserving, that is
  forall P, { P } b_n { P }.

Assume PSup is the supremum of the preconditions of b1, b2, b3, b4, .... Assume PInf is the infimum of the postconditions of b1, b2, b3, b4, .... Finally, assume you have Hoare clause judgements
  { P1 /\ PInf } a1 { Q1 /\ PSup }
  { P2 /\ PInf } a2 { Q2 /\ PSup }
...
  { Pn /\ PInf } a_n { Qn /\ PSup }

so that Q1 implies P2, Q2 implies P3, and so forth.

The conclusion is that the program (a1 `seq` a2 `seq` a3 ...) `par` (b1 `seq` b2 `seq` b3 ...) has Hoare judgement:
  { P1 /\ PSup } ... { Qn /\ PInf }.

By JamesCandy

See also: StateLaws

CategoryConcurrency