Examples

Require Import Vbase Varith Vlistbase Vlist extralib.
Require Import c11 exps rslassn rslassnlemmas rslmodel rsl.
Open Scope string_scope.

Set Implicit Arguments.

Generic lemmas

Lemma Arel_split1 x v PP :
  implies (Arel x PP)
          (Astar (Arel x PP) (Arel x (mupd (fun _ ⇒ Afalse) v (PP v)))).

Lemma Arainit_split1 x :
  implies (Arainit x)
          (Astar (Arainit x) (Arainit x)).

Lemma Arainit_split2 x :
  implies (Astar (Arainit x) (Arainit x)) (Arainit x).

Lemma Arel_split11 x PP :
  implies (Arel x PP)
          (Astar (Arel x PP) (Arel x PP)).

Lemma Armw_acq_split1 x PP QQ :
  (∀ v, QQ v = Aemp ∨ PP v = Afalse ∧ QQ v = Afalse ) →
  implies (Armwacq x PP) (Astar (Armwacq x PP) (Aacq x QQ)).

Lemma Armw_acq_split2 x PP QQ :
  (∀ v, QQ v = Aemp ∨ PP v = Afalse ∧ QQ v = Afalse ) →
  implies (Astar (Armwacq x PP) (Aacq x QQ)) (Armwacq x PP).

Lemma implies_refl P : implies P P.

Lemma implies_star_l P Q R : implies P Q → implies (Astar P R) (Astar Q R).

Lemma implies_star_r P Q R : implies P Q → implies (Astar R P) (Astar R Q).

Lemma rule_store_rel2 mt typ E E' QQ :
  release_typ typ →
  triple mt
    (Astar (Arel E QQ) (QQ E'))
    (Estore typ E E')
    (fun _ ⇒ Astar (Arel E QQ) (Arainit E)).

Lemma rule_load_rlx3 E QQ :
  triple Model_hb_rf_acyclic (Astar (Armwacq E QQ) (Arainit E))
  (Eload ATrlx E)
  (fun v ⇒ if QQ v == Afalse then Afalse else Astar (Armwacq E QQ) (Arainit E)).

Lemma rule_repeat2 mt P E QQ QQ' :
  triple mt P E QQ' →
  implies (QQ' 0) P →
  (∀ x (NZ: x ≠ 0), implies (QQ' x) (QQ x)) →
  triple mt P (Erepeat E) QQ.

Lemma implies_sim P Q : Asim P Q → implies P Q.

Lemma rule_conseq_pre :
  ∀ (mt : model_type) (P : assn) (E : cexp) (QQ : nat → assn),
    triple mt P E QQ →
    ∀ P' : assn,
      implies P' P →
      triple mt P' E QQ.

Notation " 'LET' x <- E 'IN' F " :=
  (Elet E (fun x ⇒ F))
  (at level 200, x ident).
Notation " 'REPEAT' E 'END' " := (Erepeat E).
Notation " 'PAR_BEGIN' E 'PAR' F 'END' " := (Epar E F).
Notation " [[ E ]]_ A " := (Eload A E) (at level 198, A ident).
Notation " [[ E ]]_ A <- V " := (Estore A E V) (at level 198, A ident).
Notation " E ;; F " := (Elet E (fun _ ⇒ F)) (at level 199).

Mutual exclusion locks

The first example is a mutual exclusion lock module. The lock is implemented as a location storing 0 whenever the lock is held and 1 whenever it is free.

Definition new_lock :=
  LET x <- Ealloc IN
  [[ x ]]_ ATrel <- 1 ;;
  Evalue x.

Definition spin x :=
  REPEAT [[ x ]]_ ATrlx END.

Definition lock x :=
  REPEAT spin x ;; Ecas ATacq ATrlx x 1 0 END.

Definition unlock x :=
  [[ x ]]_ ATrel <- 1.

Further, we show that an invariant J may be attached to a lock so that we get the same specifications as in concurrent separation logic.

Definition LockQQ J v :=
  if v == 0 then Aemp
  else if v == 1 then J
  else Afalse.

Definition LockPred x J :=
  Astar (Arel x (LockQQ J)) (Astar (Armwacq x (LockQQ J)) (Arainit x)).

Lemma new_lock_spec mt J :
  triple mt J new_lock (fun x ⇒ LockPred x J).

Lemma unlock_spec mt x J :
  triple mt (Astar (LockPred x J) J) (unlock x) (fun _ ⇒ LockPred x J).

Lemma spin_spec mt x J :
  triple mt (LockPred x J) (spin x) (fun _ ⇒ LockPred x J).

Lemma lock_spec x J :
  triple Model_hb_rf_acyclic
         (LockPred x J) (lock x) (fun _ ⇒ Astar (LockPred x J) J).

Lemma precise_pt a b : precise (Apt a b).

Fixpoint has_no_rlx_writes E :=
  match E with
    | Evalue _ | Ealloc | Eload _ _ ⇒ True
    | Estore typ _ _ | Ecas typ _ _ _ _ ⇒ typ ≠ ATrlx ∧ typ ≠ ATacq
    | Elet E1 E2 ⇒ has_no_rlx_writes E1 ∧ ∀ v, has_no_rlx_writes (E2 v)
    | Epar E1 E2 ⇒ has_no_rlx_writes E1 ∧ has_no_rlx_writes E2
    | Erepeat E ⇒ has_no_rlx_writes E
  end.

Lemma triple_false mt E QQ :
  mt = Model_hb_rf_acyclic ∨ has_no_rlx_writes E →
  triple mt Afalse E QQ.

Message passing

The second example is a two-thread message passing program. The first thread initializes location a and performs a release write to channel c signalling that a is initialized. The second thread waits in a busy loop performing acquire reads from c until it notices the first thread's signal. It then accesses and updates the value of a.

Lemma mp_example mt :
  triple mt Aemp
    (LET a <- Ealloc IN
     LET c <- Ealloc IN
     [[c]]_ATrel <- 0 ;;
     PAR_BEGIN
         [[a]]_ATna <- 7 ;;
         [[c]]_ATrel <- 1
     PAR
         REPEAT [[c]]_ATacq END ;;
         LET v <- [[a]]_ATna IN
         [[a]]_ATna <- v + 1
     END ;;
     [[a]]_ATna)
    (fun v ⇒ if v == 8 then Atrue else Afalse).

This page has been generated by coqdoc Imprint | Data protection