Results about sequential consistency

Require Import Classical List Permutation Relations Peano_dec Setoid Omega.
Require Import Vbase extralib ExtraRelations cactions WMModels.
Set Implicit Arguments.

Lemma ConsistentMO_dom_restr_eq lab mo :
  ConsistentMO_big_dom lab mo →
  ConsistentMO_dom lab (restr_eq_rel (fun x : actid ⇒ loc (lab x)) mo).

Lemma is_total_restr_eq X lab (mo : relation X) l :
  is_total (fun a ⇒ is_write (lab a)) mo →
  is_total (fun a ⇒ is_writeL (lab a) l) (restr_eq_rel (fun x ⇒ loc (lab x)) mo).

Equivalent SC definitions

We show that all the presented alternative definitions of sequential consistency are equivalent to one another.

1. The total order version is equivalent to the (po U rf U mo U rb)-acyclic version.

Theorem ModelSC_total_mo lab sb rf :
(∃ mo, ModelSC_total lab sb rf mo ) ↔
(∃ mo, ModelSC_mo lab sb rf mo ).

2. The total order version is equivalent to the paper's version.

Theorem ModelSC_total_bigmo lab sb rf :
(∃ mo, ModelSC_total lab sb rf mo ) ↔
(∃ mo, ModelSC_bigmo lab sb rf mo ).

3. The paper's version is equivalent to a simplified version.

Theorem ModelSC_bigmo_simplify lab sb (T: transitive sb) rf mo :
ModelSC_bigmo lab sb rf mo ↔
ModelSC_bigmo_simpl lab sb rf mo.

The same theorems about SC-consistency of plain executions.

Corollary ConsistentSC_total_mo pe :
  Consistent ModelSC_total pe ↔
  Consistent ModelSC_mo pe.

Corollary ConsistentSC_total_bigmo pe :
  Consistent ModelSC_total pe ↔
  Consistent ModelSC_bigmo pe.

This page has been generated by coqdoc