Adequacy

The consistent executions of a closed program are given as follows.

Adequacy states that all consistent executions of closed programs, e, satisfying the triple {Atrue} e {y. QQ y}, are memory safe and race free. Moreover, the programs never read from uninitialized locations, and their return value satisfies the post-condition.

Soundness of the proof rules

We now proceed with the proofs of the various RSL proof rules. For conciseness, all the internal lemmas used in these proofs are in rslmodel.v.

Frame

Consequence

Disjunction

Existential quantification

Values

Sequential composition (let)

Parallel composition

Loops

Non-atomic allocations

Non-atomic stores

Note that besides non-atomic stores, we can also use release and SC atomic stores as these are stronger than the non-atomic ones.

Non-atomic loads

Due to the causality cycle problem, in the standard model relaxed and non-atomic reads are incomparable: this is why we cannot use a relaxed reads in this rule.

Atomic allocations

Release stores

Relaxed stores

We do not allow any relaxed stores in the standard model because of the causality cycle problem. The following rule is applicable only to relaxed stores in Model_hb_rf_acyclic.

Relaxed loads

We have two rules for relaxed loads. First, we have a very weak rule that asserts nothing about the value that was read.

Second, we have a stronger rule asserting that the value read was once written. Note that this stronger rule is valid only in Model_hb_rf_acyclic.

Acquire loads

Atomic RMWs: Compare and swap