Top.drf

Data race freedom

Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslassnsem fslmodel fslassnlemmas.
Require Import fslhmap path step stepback ihc memsafe.
Require Import fslhmapa fslhmapna.
Require Import permission.
Require Import Omega.

Set Implicit Arguments.

We need to establish that whenever we have two edges annotated by heaps having a location l in their domain, and one of them has a full non-atomic access to l, then those two edges are connected by a well-formed path.

First, we prove two helper lemmas.

Lemma connection_to_lvalue_forward_helper PS PSg:
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    a1 a2 b1 b2 (DIF: b2 ≠ b1) (EV1: sb a1 b1) (EV2: sb a2 b2) (IN1: In a1 V) (IN2: In a2 V)
    hf1 g1 hf2 g2 (MAP1: hmap (hb_sb a1 b1) = Hdef hf1 g1) (MAP2: hmap (hb_sb a2 b2) = Hdef hf2 g2)
    l (ALLOCATED: hf1 l ≠ @HVnone PS PSg) (LBL: HVlabeled (hf1 l) HLnormal) (LVAL: is_lvalue (hf2 l))
    (DIRECTION: clos_refl_trans _ (happens_before_union_rf sb rf) b1 a2),
  ∀ n, ∃ path c,
    << CONNECT: hbpath_connects lab sb rf ((hb_sb a1 b1 , HLnormal ) :: path) a1 c >> ∧
    << HBuRF: clos_refl_trans _ (happens_before_union_rf sb rf) c a2 >> ∧
    << TRACK: tracking_path hmap path l >> ∧
    << LEN: c = a2 ∨ length path = n >>.

Lemma connection_to_lvalue_backwards_helper PS PSg:
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    a1 a2 b1 b2 (DIF: b1 ≠ b2) (EV1: sb a1 b1) (EV2: sb a2 b2) (IN1: In a1 V) (IN2: In a2 V)
    hf1 g1 hf2 g2 (MAP1: hmap (hb_sb a1 b1) = Hdef hf1 g1) (MAP2: hmap (hb_sb a2 b2) = Hdef hf2 g2)
    l (LVAL: is_lvalue (hf1 l)) (ALLOCATED: hf2 l ≠ @HVnone PS PSg) (LBL: HVlabeled (hf2 l) HLnormal)
    (DIRECTION: clos_refl_trans _ (happens_before_union_rf sb rf) b1 a2),
  ∀ n, ∃ path c,
    << CONNECT: hbpath_connects lab sb rf (path ++ (hb_sb a2 b2 , HLnormal ) :: nil) c b2 >> ∧
    << HBuRF: clos_refl_trans _ (happens_before_union_rf sb rf) b1 c >> ∧
    << TRACK: tracking_path hmap path l >> ∧
    << LEN: c = b1 ∨ length path = n >>.

Now, we prove two lemmas showing how a tracking path can always be extended to an adjacent edge having a full nonatomic permission.

Lemma lvalue_before_path PS PSg:
  ∀ acts lab sb rf mo hmap
    (FIN: ExecutionFinite acts lab sb)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    V (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    a b (IN: In a V)
    path (CONNECT: hbpath_connects lab sb rf path a b)
    l (TRACK: tracking_path hmap path l)
    edge (EV: edge_valid lab sb rf edge) (SND: hb_snd edge = Some a)
    hf g (MAP: hmap edge = @Hdef PS PSg hf g) (LVAL: is_lvalue (hf l)),
  hbpath_connects lab sb rf ((edge , HLnormal ) :: path) (hb_fst edge) b ∧
  tracking_path hmap ((edge , HLnormal ) :: path) l.

Lemma lvalue_after_path PS PSg :
  ∀ acts lab sb rf mo hmap
    (FIN: ExecutionFinite acts lab sb)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    V (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    hf g (MAP: hmap edge = @Hdef PS PSg hf g) l (LVAL: is_lvalue (hf l))
    a path (CONNECT: hbpath_connects lab sb rf path a (hb_fst edge))
    (TRACK: tracking_path hmap path l)
    b (SND: hb_snd edge = Some b),
  hbpath_connects lab sb rf (path ++ (edge , HLnormal ) :: nil) a b ∧
  tracking_path hmap (path ++ (edge , HLnormal ) :: nil) l.

The main connectedness lemma.

Lemma connection_to_lvalue PS PSg:
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    a1 a2 b1 b2 (DIF: b1 ≠ b2) (EV1: sb a1 b1) (EV2: sb a2 b2) (IN1: In a1 V) (IN2: In a2 V)
    hf1 g1 hf2 g2 (MAP1: hmap (hb_sb a1 b1) = Hdef hf1 g1) (MAP2: hmap (hb_sb a2 b2) = Hdef hf2 g2)
    l (LVAL: is_lvalue (hf1 l)) (ALLOCATED: hf2 l ≠ @HVnone PS PSg) (LBL: HVlabeled (hf2 l) HLnormal),
  ∃ path, hbpath_wf lab sb rf ((hb_sb a1 b1 , HLnormal ) :: path ++ (hb_sb a2 b2 , HLnormal ) :: nil) ∨
               hbpath_wf lab sb rf ((hb_sb a2 b2 , HLnormal ) :: path ++ (hb_sb a1 b1 , HLnormal ) :: nil) .

A location is either used atomically or non-atomically

Lemma atomicity_is_exclusive PS PSg (hv: HeapVal PS PSg): is_atomic hv → is_nonatomic hv → False.

Lemma atomicity_is_globally_exclusive PS PSg:
  ∀ lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge1 (EV1: edge_valid lab sb rf edge1) (IN1: In (hb_fst edge1) V)
    hf1 g1 (MAP1: hmap edge1 = Hdef hf1 g1)
    edge2 (EV2: edge_valid lab sb rf edge2) (IN2: In (hb_fst edge2) V)
    hf2 g2 (MAP2: hmap edge2 = @Hdef PS PSg hf2 g2)
    l (AT: is_atomic (hf1 l)) (NA: is_nonatomic (hf2 l)),
  False.

The main race-freedom theorem

Theorem valid_implies_race_free PS PSg :
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VALID: @hmap_valids PS PSg lab sb rf hmap V),
  race_free V lab sb rf mo.

This page has been generated by coqdoc