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 : actidloc (lab x)) mo).

Lemma is_total_restr_eq X lab (mo : relation X) l :
  is_total (fun ais_write (lab a)) mo
  is_total (fun ais_writeL (lab a) l) (restr_eq_rel (fun xloc (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.
3. The paper's version is equivalent to a simplified version.
The same theorems about SC-consistency of plain executions.

This page has been generated by coqdoc