Library Programs

Require Import Bool.
Require Import HahnBase.
Require Import Heaps.
Require Import List.
Require Import Morphisms.
Require Import Permissions.
Require Import Prelude.
Require Import Process.
Require Import ProcMap.
Require Import Setoid.

Import ListNotations.

Set Implicit Arguments.

Programs

Module Type Programs
  (dom : Domains)
  (heaps : Heaps dom)
  (procs : Processes dom)
  (procmaps : ProcMaps dom heaps procs).

Export dom heaps procs procmaps.

Statics

Expressions

Inductive Expr :=
  | Econst(v : Val)
  | Evar(x : Var)
  | Eop(E1 E2 : Expr).

Add Search Blacklist "Expr_rect".
Add Search Blacklist "Expr_ind".
Add Search Blacklist "Expr_rec".
Add Search Blacklist "Expr_sind".

Below is a helper tactic for doing induction on the structure of (program) expressions.

Ltac expr_induction E :=
  induction E as [

    v|

    x|

    E1 IH1 E2 IH2
  ].

Expressions have decidable equality.

Lemma expr_eq_dec :
forall E1 E2 : Expr, { E1 = E2 } + { E1 <> E2 }.

Conversions

The following operation converts process expressions to program expressions.

Fixpoint pexpr_convert (e : ProcExpr)(f : ProcVar -> Expr) : Expr :=
  match e with
    | PEconst v => Econst v
    | PEvar x => f x
    | PEop e1 e2 => Eop (pexpr_convert e1 f) (pexpr_convert e2 f)
  end.

Free variables

Free variables of expressions are defined in the standard way.

Fixpoint expr_fv (E : Expr) : list Var :=
   match E with
    | Econst v => []
    | Evar x => [x]
    | Eop E1 E2 => expr_fv E1 ++ expr_fv E2
  end.

Definition expr_map_fv {T} (f : T -> Expr)(x : Var) : Prop :=
  exists t : T, In x (expr_fv (f t)).

Substitution

Substitution within expressions is defined in the standard way.

Fixpoint expr_subst (x : Var)(E E' : Expr) : Expr :=
  match E' with
    | Econst v => Econst v
    | Evar y => if var_eq_dec x y then E else Evar y
    | Eop E1 E2 => Eop (expr_subst x E E1) (expr_subst x E E2)
  end.

Definition expr_subst_map {T} (x : Var)(E : Expr)(f : T -> Expr) : T -> Expr :=
  fun y : T => expr_subst x E (f y).

Standard properties of substitution.

Lemma expr_subst_pres :
  forall E1 E2 x, ~ In x (expr_fv E1) -> expr_subst x E2 E1 = E1.

Lemma expr_subst_pres_map {T} :
  forall (f : T -> Expr) E x,
  ~ expr_map_fv f x -> expr_subst_map x E f = f.

Lemma expr_subst_comm :
  forall E x1 x2 E1 E2,
  x1 <> x2 ->
  ~ In x1 (expr_fv E2) ->
  ~ In x2 (expr_fv E1) ->
  expr_subst x1 E1 (expr_subst x2 E2 E) =
  expr_subst x2 E2 (expr_subst x1 E1 E).

Lemma expr_subst_comm_val :
  forall E x1 x2 v1 v2,
  x1 <> x2 ->
  expr_subst x1 (Econst v1) (expr_subst x2 (Econst v2) E) =
  expr_subst x2 (Econst v2) (expr_subst x1 (Econst v1) E).

Hybrid expressions

Hybrid expressions are expressions that have both program variables and process variables (and are thus a hybrid between Expr and ProcExpr).

Inductive HExpr :=
  | HEconst(v : Val)
  | HEprocvar(x : ProcVar)
  | HEprogvar(x : Var)
  | HEop(E1 E2 : HExpr).

Add Search Blacklist "HExpr_rect".
Add Search Blacklist "HExpr_ind".
Add Search Blacklist "HExpr_rec".
Add Search Blacklist "HExpr_sind".

Below is a helper tactic for doing induction on the structure of hybrid expressions.

Ltac hexpr_induction E :=
induction E as [v|x|x|E1 IH1 E2 IH2].

Free variables

The following operation determines the set of free program variables in a hybrid expression.

Fixpoint hexpr_fv (E : HExpr) : list Var :=
  match E with
    | HEconst _ => []
    | HEprocvar _ => []
    | HEprogvar x => [x]
    | HEop E1 E2 => hexpr_fv E1 ++ hexpr_fv E2
  end.

And the following is for determining the set of free process variables in hybrid expressions

Fixpoint hexpr_fpv (E : HExpr) : list ProcVar :=
  match E with
    | HEconst _ => []
    | HEprocvar x => [x]
    | HEprogvar _ => []
    | HEop E1 E2 => hexpr_fpv E1 ++ hexpr_fpv E2
  end.

Hybridisation

The following operation allows to make a hybrid expression out of an ordinary expression.

Fixpoint peHybridise (e : ProcExpr) : HExpr :=
  match e with
    | PEconst v => HEconst v
    | PEvar x => HEprocvar x
    | PEop e1 e2 => HEop (peHybridise e1) (peHybridise e2)
  end.

Fixpoint eHybridise (E : Expr) : HExpr :=
  match E with
    | Econst v => HEconst v
    | Evar x => HEprogvar x
    | Eop E1 E2 => HEop (eHybridise E1) (eHybridise E2)
  end.

Conversions

Below is an operation that converts hybrid expressions to ordinary program expressions.

Fixpoint hexpr_convert (E : HExpr)(f : ProcVar -> Expr) : Expr :=
  match E with
    | HEconst v => Econst v
    | HEprocvar x => f x
    | HEprogvar x => Evar x
    | HEop E1 E2 => Eop (hexpr_convert E1 f) (hexpr_convert E2 f)
  end.

Conditions

Inductive Cond :=
  | Bconst(b : bool)
  | Bnot(B : Cond)
  | Band(B1 B2 : Cond)
  | Beq(E1 E2 : Expr).

Add Search Blacklist "Cond_rect".
Add Search Blacklist "Cond_ind".
Add Search Blacklist "Cond_rec".
Add Search Blacklist "Cond_sind".

Below is a helper tactic for doing induction on the structure of (program) conditions.

Ltac cond_induction B :=
  induction B as [

    b|

    B IH|

    B1 IH1 B2 IH2|

    E1 E2
  ].

Conditions have decidable equality.

Lemma cond_eq_dec :
forall B1 B2 : Cond, { B1 = B2 } + { B1 <> B2 }.

Some sugar

Definition Bor B1 B2 := Bnot (Band (Bnot B1) (Bnot B2)).
Definition Bimplies B1 B2 := Bor (Bnot B1) B2.
Definition Bequiv B1 B2 := Band (Bimplies B1 B2) (Bimplies B2 B1).

Conversions

The following operation converts process conditions to program conditions.

Fixpoint pcond_convert (b : ProcCond)(f : ProcVar -> Expr) : Cond :=
  match b with
    | PBconst b' => Bconst b'
    | PBnot b' => Bnot (pcond_convert b' f)
    | PBand b1 b2 => Band (pcond_convert b1 f) (pcond_convert b2 f)
    | PBeq e1 e2 => Beq (pexpr_convert e1 f) (pexpr_convert e2 f)
  end.

Free variables

Free variables of conditions are defined in the standard way.

Fixpoint cond_fv (B : Cond) : list Var :=
   match B with
    | Bconst b => nil
    | Bnot B' => cond_fv B'
    | Band B1 B2 => cond_fv B1 ++ cond_fv B2
    | Beq E1 E2 => expr_fv E1 ++ expr_fv E2
  end.

Substitution

Substitution within conditions is defined in the standard way.

Fixpoint cond_subst (x : Var)(E : Expr)(B : Cond) : Cond :=
  match B with
    | Bconst b => Bconst b
    | Bnot B' => Bnot (cond_subst x E B')
    | Band B1 B2 => Band (cond_subst x E B1) (cond_subst x E B2)
    | Beq E1 E2 => Beq (expr_subst x E E1) (expr_subst x E E2)
  end.

Standard properties of substitution.

Lemma cond_subst_pres :
forall B E x, ~ In x (cond_fv B) -> cond_subst x E B = B.

Hybrid conditions

Hybrid conditions are conditions that have both program variables and process variables (and are thus a hybrid between Cond and ProcCond).

Inductive HCond :=
  | HBconst(b : bool)
  | HBnot(B : HCond)
  | HBand(B1 B2 : HCond)
  | HBeq(E1 E2 : HExpr).

Add Search Blacklist "HCond_rect".
Add Search Blacklist "HCond_ind".
Add Search Blacklist "HCond_rec".
Add Search Blacklist "HCond_sind".

Below is a helper tactic for doing induction on the structure of hybrid conditions.

Ltac hcond_induction B :=
  induction B as [

    b|

    B IH|

    B1 IH1 B2 IH2|

    E1 E2
  ].

Free variables

The following operation determines the set of free program variables in a hybrid condition.

Fixpoint hcond_fv (B : HCond) : list Var :=
  match B with
    | HBconst _ => []
    | HBnot B' => hcond_fv B'
    | HBand B1 B2 => hcond_fv B1 ++ hcond_fv B2
    | HBeq E1 E2 => hexpr_fv E1 ++ hexpr_fv E2
  end.

And the following operation determines the set of free process variables in hybrid conditions.

Fixpoint hcond_fpv (B : HCond) : list ProcVar :=
  match B with
    | HBconst _ => []
    | HBnot B' => hcond_fpv B'
    | HBand B1 B2 => hcond_fpv B1 ++ hcond_fpv B2
    | HBeq E1 E2 => hexpr_fpv E1 ++ hexpr_fpv E2
  end.

Hybridisation

The following operation enables one to construct hybrid conditions out of ordinary (program) conditions.

Fixpoint pcHybridise (b : ProcCond) : HCond :=
  match b with
    | PBconst v => HBconst v
    | PBnot b' => HBnot (pcHybridise b')
    | PBand b1 b2 => HBand (pcHybridise b1) (pcHybridise b2)
    | PBeq e1 e2 => HBeq (peHybridise e1) (peHybridise e2)
  end.

Fixpoint cHybridise (B : Cond) : HCond :=
  match B with
    | Bconst v => HBconst v
    | Bnot B' => HBnot (cHybridise B')
    | Band B1 B2 => HBand (cHybridise B1) (cHybridise B2)
    | Beq E1 E2 => HBeq (eHybridise E1) (eHybridise E2)
  end.

Conversions

The following operation is for converting hybrid conditions to ordinary program conditions.

Fixpoint hcond_convert (B : HCond)(f : ProcVar -> Expr) : Cond :=
  match B with
    | HBconst b => Bconst b
    | HBnot B' => Bnot (hcond_convert B' f)
    | HBand B1 B2 => Band (hcond_convert B1 f) (hcond_convert B2 f)
    | HBeq E1 E2 => Beq (hexpr_convert E1 f) (hexpr_convert E2 f)
  end.

Hybrid processes

Hybrid processes P are ordinary processes in which any (Boolean) expression occuring inside P may contain program variables (in addition to process variables).

Below is a shorthand tactic for doing induction on the inductive structure of hybrid processes.

Free variables

Hybridisation

The following operation enables one to construct a hybrid process out of an ordinary process.

Commands

Commands are parameterised by a type, which is the type of the metadata that is stored in action blocks (see the Cinact constructor). We later define a ghost operational semantics (in which the metadata component is used to maintain extra runtime information regarding abstract models.

A shorthand for doing induction over commands:

Ltac cmd_induction C :=
  induction C as [|

    C1 IH1 C2 IH2|

    x E|

    x E|

    E1 E2|

    B C1 IH1 C2 IH2|

    B C IH|

    C1 IH1 C2 IH2|

    x E|

    E|

    C IH|
    C IH|

    x Pf E xs f|

    x a E C IH|
    m C IH|

    x|

    x
  ].

Some standard properties over the structure of commands.

Lemma cmd_neg_seq {T} :
  forall C2 C1 : Cmd T, ~ C2 = Cseq C1 C2.

Lemma cmd_neg_ite_t {T} :
  forall (C1 C2 : Cmd T) B, ~ C1 = Cite B C1 C2.

Lemma cmd_neg_ite_f {T} :
  forall (C2 C1 : Cmd T) B, ~ C2 = Cite B C1 C2.

Plain commands

Plain commands are commands without metadata components (or, technically, these are commands in which the metadata type is fixed and chosen to have only one inhabitant, namely PMnone).

Inductive PlainMetadata := PMnone.

Add Search Blacklist "PlainMetadata_rec".
Add Search Blacklist "PlainMetadata_ind".
Add Search Blacklist "PlainMetadata_rect".
Add Search Blacklist "PlainMetadata_sind".

Definition PlainCmd : Type := Cmd PlainMetadata.

Fixpoint plain {T} (C : Cmd T) : PlainCmd :=
  match C with
    | Cskip => Cskip
    | Cseq C1 C2 => Cseq (plain C1) (plain C2)
    | Cass x E => Cass x E
    | Cread x E => Cread x E
    | Cwrite E1 E2 => Cwrite E1 E2
    | Cite B C1 C2 => Cite B (plain C1) (plain C2)
    | Cwhile B C' => Cwhile B (plain C')
    | Cpar C1 C2 => Cpar (plain C1) (plain C2)
    | Calloc x E => Calloc x E
    | Cdispose E => Cdispose E
    | Catomic C' => Catomic (plain C')
    | Cinatom C' => Cinatom (plain C')
    | Cproc x P E xs f => Cproc x P E xs f
    | Cact x a E C' => Cact x a E (plain C')
    | Cquery x => Cquery x
    | Cinact _ C' => Cinact PMnone (plain C')
    | Cendproc x => Cendproc x
  end.

Lemma plain_skip {T} :
  forall C : Cmd T, plain C = Cskip -> C = Cskip.

User programs

Any program is a user program if it does not contain Cinact or Cinatom as a subprogram.

The program Cinatom C represents an atomic program C that is only partially executed. Such programs cannot be written by a user but are an artifact of the program dynamics. The same holds for Cinact m C, which describes a partially executed action program C (and is a specification-only command besides).

Fixpoint cmd_user {T} (C : Cmd T) : Prop :=
  match C with
    | Cskip => True
    | Cseq C1 C2 => cmd_user C1 /\ cmd_user C2
    | Cass _ _ => True
    | Cread _ _ => True
    | Cwrite _ _ => True
    | Cite _ C1 C2 => cmd_user C1 /\ cmd_user C2
    | Cwhile _ C' => cmd_user C'
    | Cpar C1 C2 => cmd_user C1 /\ cmd_user C2
    | Calloc _ _ => True
    | Cdispose _ => True
    | Catomic C' => cmd_user C'
    | Cinatom _ => False
    | Cproc _ _ _ _ _ => True
    | Cact _ _ _ C' => cmd_user C'
    | Cquery _ => True
    | Cinact _ _ => False
    | Cendproc _ => True
  end.

Lemma cmd_user_plain {T} :
  forall C : Cmd T, cmd_user C = cmd_user (plain C).

Locked programs

Any program is defined to be locked if it contains Cinatom as a subprogram.

Fixpoint cmd_locked {T} (C : Cmd T) : Prop :=
  match C with
    | Cseq C1 _ => cmd_locked C1
    | Cpar C1 C2 => cmd_locked C1 \/ cmd_locked C2
    | Cinact _ C1 => cmd_locked C1
    | Cinatom _ => True
    | _ => False
  end.

Lemma cmd_locked_plain {T} :
  forall C : Cmd T, cmd_locked (plain C) = cmd_locked C.

Well-formed programs

Any program is defined to be basic if it does not contain any process-related commands, and if there are no deadlocks in any of its parallel subprograms.

Any program is well-formed if C is basic for every subcommand Cact _ _ C that occurs in the program, and if there are no deadlocks in any of its parallel subprograms, likewise to basic programs.

Fixpoint cmd_basic {T} (C : Cmd T) : Prop :=
  match C with
    | Cskip => True
    | Cseq C1 C2 => cmd_basic C1 /\ cmd_basic C2
    | Cass _ _ => True
    | Cread _ _ => True
    | Cwrite _ _ => True
    | Cite _ C1 C2 => cmd_basic C1 /\ cmd_basic C2
    | Cwhile _ C' => cmd_basic C'
    | Cpar C1 C2 => cmd_basic C1 /\ cmd_basic C2 /\ ~ (cmd_locked C1 /\ cmd_locked C2)
    | Calloc _ _ => True
    | Cdispose _ => True
    | Catomic C' => cmd_basic C'
    | Cinatom C' => cmd_basic C'
    | Cproc _ _ _ _ _ => False
    | Cact _ _ _ _ => False
    | Cinact _ _ => False
    | Cquery _ => False
    | Cendproc _ => False
  end.

Fixpoint cmd_wf {T} (C : Cmd T) : Prop :=
  match C with
    | Cskip => True
    | Cseq C1 C2 => cmd_wf C1 /\ cmd_wf C2
    | Cass _ _ => True
    | Cread _ _ => True
    | Cwrite _ _ => True
    | Cite _ C1 C2 => cmd_wf C1 /\ cmd_wf C2
    | Cwhile _ C' => cmd_wf C'
    | Cpar C1 C2 => cmd_wf C1 /\ cmd_wf C2 /\ ~ (cmd_locked C1 /\ cmd_locked C2)
    | Calloc _ _ => True
    | Cdispose _ => True
    | Catomic C' => cmd_wf C'
    | Cinatom C' => cmd_wf C'
    | Cproc _ _ _ _ _ => True
    | Cact _ _ _ C' => cmd_basic C'
    | Cinact _ C' => cmd_basic C'
    | Cquery _ => True
    | Cendproc _ => True
  end.

Any basic program is well-formed.

Lemma cmd_basic_wf {T} :
forall C : Cmd T, cmd_basic C -> cmd_wf C.

Free variables

The free variables of commands are defined in the standard way.

Fixpoint cmd_fv {T} (C : Cmd T)(x : Var) : Prop :=
  match C with
    | Cskip => False
    | Cass y E
    | Cread y E
    | Calloc y E => x = y \/ In x (expr_fv E)
    | Cwrite E1 E2 => In x (expr_fv E1) \/ In x (expr_fv E2)
    | Cite B C1 C2 => In x (cond_fv B) \/ cmd_fv C1 x \/ cmd_fv C2 x
    | Cwhile B C' => In x (cond_fv B) \/ cmd_fv C' x
    | Cseq C1 C2
    | Cpar C1 C2 => cmd_fv C1 x \/ cmd_fv C2 x
    | Cdispose E => In x (expr_fv E)
    | Catomic C'
    | Cinatom C' => cmd_fv C' x
    | Cproc y P E xs f =>
        x = y \/ In x (expr_fv E) \/ expr_map_fv f x \/
        exists v, hproc_fv (P v) x
    | Cact y _ E C' => x = y \/ In x (expr_fv E) \/ cmd_fv C' x
    | Cinact _ C' => cmd_fv C' x
    | Cquery y => x = y
    | Cendproc y => x = y
  end.

Lemma cmd_fv_plain {T} :
  forall C : Cmd T, cmd_fv C = cmd_fv (plain C).

Modified variables

The operation cmd_mod captures the set of variables that are modified (written to) by a given program, and is defined in the standard way (however, note that, for later convenience, cmd_mod is defined as a predicate, rather than a fixpoint operation that yields a list of variables).

Fixpoint cmd_mod {T} (C : Cmd T)(x : Var) : Prop :=
  match C with
    | Cskip => False
    | Cass y _
    | Cread y _ => x = y
    | Cwrite _ _ => False
    | Cseq C1 C2
    | Cpar C1 C2
    | Cite _ C1 C2 => cmd_mod C1 x \/ cmd_mod C2 x
    | Cwhile _ C' => cmd_mod C' x
    | Calloc y _ => x = y
    | Cdispose _ => False
    | Catomic C' => cmd_mod C' x
    | Cinatom C' => cmd_mod C' x
    | Cproc y _ _ _ _ => x = y
    | Cact _ _ _ C'
    | Cinact _ C' => cmd_mod C' x
    | Cquery _ => False
    | Cendproc _ => False
  end.

All variables written to by C occur freely in C.

Lemma cmd_fv_mod {T} :
forall (C : Cmd T)(x : Var), cmd_mod C x -> cmd_fv C x.

Lemma cmd_mod_plain {T} :
forall C : Cmd T, cmd_mod C = cmd_mod (plain C).

Dynamics

Stores

Definition Store := Var -> Val.

An update operation for stores:

Definition sUpdate (s : Store)(x : Var)(v : Val) : Store :=
  update var_eq_dec s x v.

Lemma sUpdate_comm :
  forall s x1 v1 x2 v2,
  x1 <> x2 ->
  sUpdate (sUpdate s x1 v1) x2 v2 =
  sUpdate (sUpdate s x2 v2) x1 v1.

The following definition captures two stores agreeing on a given predicate phi over (program) variables.

Definition sAgree (phi : Var -> Prop)(s1 s2 : Store) : Prop :=
forall x, phi x -> s1 x = s2 x.

Store agreement is a symmetric relation.

Global Instance sAgree_symm :
forall phi, Symmetric (sAgree phi).

Below are several other useful properties of store agreement.

Lemma sAgree_split :
  forall phi1 phi2 s1 s2,
  sAgree (fun x => phi1 x \/ phi2 x) s1 s2 <->
  sAgree phi1 s1 s2 /\ sAgree phi2 s1 s2.

Lemma sAgree_app :
  forall xs1 xs2 s1 s2,
  sAgree (fun x => In x (xs1 ++ xs2)) s1 s2 <->
  sAgree (fun x => In x xs1) s1 s2 /\
  sAgree (fun x => In x xs2) s1 s2.

Lemma sAgree_weaken :
  forall (phi1 phi2 : Var -> Prop)(s1 s2 : Store),
    (forall x, phi1 x -> phi2 x) ->
  sAgree phi2 s1 s2 ->
  sAgree phi1 s1 s2.

Denotational semantics

Expressions

Fixpoint expr_eval (E : Expr)(s : Store) : Val :=
  match E with
    | Econst v => v
    | Evar x => s x
    | Eop E1 E2 => val_op (expr_eval E1 s) (expr_eval E2 s)
  end.

Definition expr_eval_map {T} (f : T -> Expr)(s : Store) : T -> Val :=
  fun x : T => expr_eval (f x) s.

Standard properties relating substitution to evaluation:

Lemma expr_eval_subst :
  forall E2 E1 x s,
  expr_eval (expr_subst x E1 E2) s =
  expr_eval E2 (sUpdate s x (expr_eval E1 s)).

Lemma expr_eval_subst_map {T} :
  forall (f : T -> Expr) E x s,
  expr_eval_map (expr_subst_map x E f) s =
  expr_eval_map f (sUpdate s x (expr_eval E s)).

The following lemma relates the evaluation of process expressions with the evaluation of program expressions.

Lemma expr_eval_conv :
  forall (e : ProcExpr)(ps : ProcStore)(s : Store)(f : ProcVar -> Expr),
    (forall x : ProcVar, In x (pexpr_fv e) -> ps x = expr_eval (f x) s) ->
  expr_eval (pexpr_convert e f) s = pexpr_eval e ps.

The evaluation of expressions only depends on its free variables.

Lemma expr_agree :
  forall E s1 s2,
  sAgree (fun x => In x (expr_fv E)) s1 s2 ->
  expr_eval E s1 = expr_eval E s2.

Lemma expr_map_agree {T} :
  forall (f : T -> Expr) s1 s2,
    (forall x, expr_map_fv f x -> s1 x = s2 x) ->
  expr_eval_map f s1 = expr_eval_map f s2.

The following lemma relates expression evaluation to store updates.

Lemma expr_eval_upd :
  forall E s x v,
  ~ In x (expr_fv E) ->
  expr_eval E (sUpdate s x v) = expr_eval E s.

Other useful properties of expression evaluation.

Lemma expr_eval_const :
forall E s, expr_eval E s = expr_eval (Econst (expr_eval E s)) s.

Conditions

Fixpoint cond_eval (B : Cond)(s : Store) : bool :=
  match B with
    | Bconst b => b
    | Bnot B' => negb (cond_eval B' s)
    | Band B1 B2 => (cond_eval B1 s) && (cond_eval B2 s)
    | Beq E1 E2 => if val_eq_dec (expr_eval E1 s) (expr_eval E2 s) then true else false
  end.

Lemma cond_eval_excl :
  forall B s, cond_eval B s = true \/ cond_eval B s = false.

A standard property that relates substitution to evaluation:

Lemma cond_eval_subst :
  forall B E x s,
  cond_eval (cond_subst x E B) s =
  cond_eval B (sUpdate s x (expr_eval E s)).

The following lemma relates the evaluation of process conditions with the evaluation of program conditions.

Lemma cond_eval_conv :
  forall (b : ProcCond)(ps : ProcStore)(s : Store)(f : ProcVar -> Expr),
    (forall x : ProcVar, In x (pcond_fv b) -> ps x = expr_eval (f x) s) ->
  cond_eval (pcond_convert b f) s = pcond_eval b ps.

The evaluation of conditions only depends on its free variables.

Lemma cond_agree :
  forall B s1 s2,
  sAgree (fun x => In x (cond_fv B)) s1 s2 ->
  cond_eval B s1 = cond_eval B s2.

The following lemma relates condition evaluation to store updates.

Lemma cond_eval_upd :
  forall B s x v,
  ~ In x (cond_fv B) ->
  cond_eval B (sUpdate s x v) = cond_eval B s.

Hybrid expressions

Dehybridisation

Fixpoint eDehybridise (E : HExpr)(s : Store) : ProcExpr :=
  match E with
    | HEconst v => PEconst v
    | HEprocvar x => PEvar x
    | HEprogvar x => PEconst (s x)
    | HEop E1 E2 => PEop (eDehybridise E1 s) (eDehybridise E2 s)
  end.

The following two properties relate hybridisation to evaluation.

Lemma eHybridise_eval :
  forall E s ps,
  pexpr_eval (eDehybridise (eHybridise E) s) ps = expr_eval E s.

Lemma eHybridise_conv_eval :
  forall E s ps (f : ProcVar -> Expr),
    (forall x : ProcVar, In x (hexpr_fpv E) -> ps x = expr_eval (f x) s) ->
  expr_eval (hexpr_convert E f) s =
  pexpr_eval (eDehybridise E s) ps.

Dehybridising a hybridised process expression gives the original process expression

Lemma eDehybridise_hybridise :
forall e s, e = eDehybridise (peHybridise e) s.

The following property related dehybrisation to freely occuring process variables.

Lemma eDehybridise_fpv :
forall E s x,
In x (hexpr_fpv E) <-> In x (pexpr_fv (eDehybridise E s)).

Substitution

Substitution is defined in the standard sense.

Fixpoint hexpr_subst (x : Var)(E : Expr)(HE : HExpr) : HExpr :=
  match HE with
    | HEconst v => HEconst v
    | HEprocvar y => HEprocvar y
    | HEprogvar y =>
        if var_eq_dec x y
        then eHybridise E
        else HEprogvar y
    | HEop HE1 HE2 =>
        HEop (hexpr_subst x E HE1) (hexpr_subst x E HE2)
  end.

Substituting any (program) variable that does not occur freely inside the targetted hybrid expression does not change the expression.

Lemma hexpr_subst_pres :
forall HE x E,
~ In x (hexpr_fv HE) -> hexpr_subst x E HE = HE.

The following property relates dehybridisation to substitution.

Lemma eDehybridise_subst :
  forall HE x E s ps,
  pexpr_eval (eDehybridise (hexpr_subst x E HE) s) ps =
  pexpr_eval (eDehybridise HE (sUpdate s x (expr_eval E s))) ps.

The dehybridisation of hybrid expressions only depends on its free variables.

Lemma eDehybridise_agree :
  forall E s1 s2,
  sAgree (fun x => In x (hexpr_fv E)) s1 s2 ->
  eDehybridise E s1 = eDehybridise E s2.

Hybrid conditions

Dehybridisation

Fixpoint cDehybridise (B : HCond)(s : Store) : ProcCond :=
  match B with
    | HBconst b => PBconst b
    | HBnot B' => PBnot (cDehybridise B' s)
    | HBand B1 B2 => PBand (cDehybridise B1 s) (cDehybridise B2 s)
    | HBeq E1 E2 => PBeq (eDehybridise E1 s) (eDehybridise E2 s)
  end.

The following two properties relate hybridisation to evaluation.

Lemma cHybridise_eval :
  forall B s ps,
  pcond_eval (cDehybridise (cHybridise B) s) ps = cond_eval B s.

Lemma cHybridise_conv_eval :
  forall B s ps (f : ProcVar -> Expr),
    (forall x : ProcVar, In x (hcond_fpv B) -> ps x = expr_eval (f x) s) ->
  cond_eval (hcond_convert B f) s =
  pcond_eval (cDehybridise B s) ps.

Dehybridising a hybridised process condition gives the same condition

Lemma cDehybridise_hybridise :
forall b s, b = cDehybridise (pcHybridise b) s.

The dehybridisation of hybrid conditions only depends on its free variables.

Lemma cDehybridise_agree :
  forall B s1 s2,
  sAgree (fun x => In x (hcond_fv B)) s1 s2 ->
  cDehybridise B s1 = cDehybridise B s2.

The following property related dehybrisation to freely occuring process variables.

Lemma cDehybridise_fpv :
forall B s x,
In x (hcond_fpv B) <-> In x (pcond_fv (cDehybridise B s)).

Substitution

Fixpoint hcond_subst (x : Var)(E : Expr)(B : HCond) : HCond :=
  match B with
    | HBconst v => HBconst v
    | HBnot B' => HBnot (hcond_subst x E B')
    | HBand B1 B2 => HBand (hcond_subst x E B1) (hcond_subst x E B2)
    | HBeq E1 E2 => HBeq (hexpr_subst x E E1) (hexpr_subst x E E2)
  end.

Substituting any (program) variable that does not occur freely inside the targetted hybrid condition does not change the targetted condition.

Lemma hcond_subst_pres :
forall B x E,
~ In x (hcond_fv B) -> hcond_subst x E B = B.

The following property relates dehybridisation to substitution.

Lemma cDehybridise_subst :
  forall B x E s ps,
  pcond_eval (cDehybridise (hcond_subst x E B) s) ps =
  pcond_eval (cDehybridise B (sUpdate s x (expr_eval E s))) ps.

Hybrid processes

The following two functions, hguard and heffect, are the hybrid counterparts of the functions guard and effect that constituting the guards and effects of actions

Parameter hguard : Act -> Expr -> HCond.
Parameter heffect : Act -> Expr -> HCond.

We need to make sure that the hybrid guards and effects make sense with respect to the ordinary guards and effects of actions. This is done in terms of the following properties:

Parameter hguard_corr :
  forall a E f s,
    cond_eval (hcond_convert (hguard a E) f) s =
    cond_eval (pcond_convert (guard a (expr_eval E s)) f) s.

Parameter heffect_corr :
  forall a E f s,
    cond_eval (hcond_convert (heffect a E) f) s =
    cond_eval (pcond_convert (effect a (expr_eval E s)) f) s.

(De)hybridisation

The dehybridisation operation pDehybridise for processes transforms any hybrid process to an ordinary process:

Fixpoint pDehybridise (P : HProc)(s : Store) : Proc :=
  match P with
    | HPepsilon => Pepsilon
    | HPdelta => Pdelta
    | HPact a E => Pact a (expr_eval E s)
    | HPassert B => Passert (cDehybridise B s)
    | HPseq P1 P2 => Pseq (pDehybridise P1 s) (pDehybridise P2 s)
    | HPalt P1 P2 => Palt (pDehybridise P1 s) (pDehybridise P2 s)
    | HPpar P1 P2 => Ppar (pDehybridise P1 s) (pDehybridise P2 s)
    | HPlmerge P1 P2 => Plmerge (pDehybridise P1 s) (pDehybridise P2 s)
    | HPsum f => Psum (fun v => pDehybridise (f v) s)
    | HPcond B Q => Pcond (cond_eval B s) (pDehybridise Q s)
    | HPiter Q => Piter (pDehybridise Q s)
  end.

Dehybridising a hybridised process yields the original process.

Lemma pDehybridise_hybridise :
forall P s, P = pDehybridise (pHybridise P) s.

The dehybridisation of hybrid processes only depends on its free variables.

Lemma pDehybridise_agree :
  forall P s1 s2,
  sAgree (hproc_fv P) s1 s2 ->
  pDehybridise P s1 = pDehybridise P s2.

Substitution

The substitution operation hproc_subst x E P replaces every occurence of the program variable x by the expression E inside the hybrid process P.

Fixpoint hproc_subst (x : Var)(E : Expr)(P : HProc) : HProc :=
  match P with
    | HPepsilon => HPepsilon
    | HPdelta => HPdelta
    | HPact a E' => HPact a (expr_subst x E E')
    | HPassert B => HPassert (hcond_subst x E B)
    | HPseq P1 P2 => HPseq (hproc_subst x E P1) (hproc_subst x E P2)
    | HPalt P1 P2 => HPalt (hproc_subst x E P1) (hproc_subst x E P2)
    | HPpar P1 P2 => HPpar (hproc_subst x E P1) (hproc_subst x E P2)
    | HPlmerge P1 P2 => HPlmerge (hproc_subst x E P1) (hproc_subst x E P2)
    | HPsum f => HPsum (fun v => hproc_subst x E (f v))
    | HPcond B Q => HPcond (cond_subst x E B) (hproc_subst x E Q)
    | HPiter Q => HPiter (hproc_subst x E Q)
  end.

The definition of sigma as used in the process algebra literature to define summation can now be encoded op top of substitution.

Definition HPsigma (x : Var)(P : HProc) : HProc :=
HPsum (fun v => hproc_subst x (Econst v) P).

Substituting any (program) variable that does not occur freely inside the targetted hybrid process does not change the targetted process.

Lemma hproc_subst_pres :
forall P x E,
~ hproc_fv P x -> (hproc_subst x E P) = P.

The following property relates substitution with the dehybridisation of hybrid processes.

Lemma pDehybridise_subst :
forall P x E s,
bisim (pDehybridise (hproc_subst x E P) s) (pDehybridise P (sUpdate s x (expr_eval E s))).

Hybrid process bisimilarity

Bisimilarity of hybrid processes is lifted from the definition of bisimilarity bisim of (ordinary) processes.

Definition hbisim (P Q : HProc) : Prop :=
forall s, bisim (pDehybridise P s) (pDehybridise Q s).
Definition hbisim_f : relation (Val -> HProc) :=
pointwise_relation Val hbisim.

Notation "P ≃ Q" := (hbisim P Q) (only printing, at level 80).
Notation "f ≃ g" := (hbisim_f f g) (only printing, at level 80).

Bisimilarity of hybrid processes is an equivalence relation.

Global Instance hbisim_refl : Reflexive hbisim.
Global Instance hbisim_symm : Symmetric hbisim.
Global Instance hbisim_trans : Transitive hbisim.
Global Instance hbisim_equiv : Equivalence hbisim.

Hint Resolve hbisim_refl : core.

Global Instance hbisim_f_refl : Reflexive hbisim_f.
Global Instance hbisim_f_symm : Symmetric hbisim_f.
Global Instance hbisim_f_trans : Transitive hbisim_f.
Global Instance hbisim_f_equiv : Equivalence hbisim_f.

Hint Resolve hbisim_f_refl : core.

Add Parametric Morphism : pDehybridise
with signature hbisim ==> eq ==> bisim
as pDehybridise_bisim_mor.

Congruence properties of hybrid processes

Bisimilarity of hybrid processes is a congruence for all process-algebraic connectives (this is entirely derived from the congruence properties of bisim).

Add Parametric Morphism : HPseq
  with signature hbisim ==> hbisim ==> hbisim as hbisim_seq.
Add Parametric Morphism : HPalt
  with signature hbisim ==> hbisim ==> hbisim as hbisim_alt.
Add Parametric Morphism : HPpar
  with signature hbisim ==> hbisim ==> hbisim as hbisim_par.
Add Parametric Morphism : HPlmerge
  with signature hbisim ==> hbisim ==> hbisim as hbisim_lmerge.
Add Parametric Morphism : HPsum
  with signature hbisim_f ==> hbisim as hbisim_sum.
Add Parametric Morphism : HPcond
  with signature eq ==> hbisim ==> hbisim as hbisim_cond.
Add Parametric Morphism : HPiter
  with signature hbisim ==> hbisim as hbisim_iter.

Axiomatisation of hybrid processes

All standard bisimulation equivalences can be derived from the definition of bisim.

The most important equivalences for the remaining theory are associativity and commutativity of parallel composition, which are given below.

Theorem hbisim_par_assoc :
  forall P Q R, hbisim (HPpar P (HPpar Q R)) (HPpar (HPpar P Q) R).
Theorem hbisim_par_comm :
  forall P Q, hbisim (HPpar P Q) (HPpar Q P).
Theorem hbisim_par_epsilon_l :
  forall P, hbisim (HPpar HPepsilon P) P.
Theorem hbisim_par_epsilon_r :
  forall P, hbisim (HPpar P HPepsilon) P.

Theorem hbisim_sigma_alt :
  forall P E x,
  hbisim (HPsigma x P) (HPalt (hproc_subst x E P) (HPsigma x P)).

Shared memory accesses

The operation cmd_acc C s defines the set of heap locations that are accessed by the program C in a single execution step, where s is used to evaluate all expressions referring to heap locations.

Likewise, the operation cmd_writes C s determines the set of heap locations that are written to by C in a single execution step. Note that, rather than yielding a set of heap locations, both these operations are defined as predicates instead for later convenience.

Fixpoint cmd_acc {T} (C : Cmd T)(s : Store)(l : Val) : Prop :=
  match C with
    | Cskip => False
    | Cseq C' _ => cmd_acc C' s l
    | Cass _ _ => False
    | Cread _ E
    | Cwrite E _ => l = expr_eval E s
    | Cite _ _ _
    | Cwhile _ _ => False
    | Cpar C1 C2 => cmd_acc C1 s l \/ cmd_acc C2 s l
    | Calloc _ _ => False
    | Cdispose E => l = expr_eval E s
    | Catomic _ => False
    | Cinatom C' => cmd_acc C' s l
    | Cproc _ _ _ xs f => exists x, In x xs /\ l = expr_eval (f x) s
    | Cact _ _ _ C' => False
    | Cinact _ C' => cmd_acc C' s l
    | Cquery _ => False
    | Cendproc _ => False
  end.

Fixpoint cmd_writes {T} (C : Cmd T)(s : Store)(l : Val) : Prop :=
  match C with
    | Cskip => False
    | Cseq C' _ => cmd_writes C' s l
    | Cass _ _
    | Cread _ _ => False
    | Cwrite E _ => l = expr_eval E s
    | Cite _ _ _
    | Cwhile _ _ => False
    | Cpar C1 C2 => cmd_writes C1 s l \/ cmd_writes C2 s l
    | Calloc _ _ => False
    | Cdispose E => l = expr_eval E s
    | Catomic _ => False
    | Cinatom C' => cmd_writes C' s l
    | Cproc _ _ _ _ _
    | Cact _ _ _ _ => False
    | Cinact _ C' => cmd_writes C' s l
    | Cquery _ => False
    | Cendproc _ => False
  end.

All writes to shared memory are also shared-memory accesses.

Lemma cmd_writes_acc {T} :
forall (C : Cmd T) s l, cmd_writes C s l -> cmd_acc C s l.

Other useful properties of shared-memory accesses.

Lemma cmd_acc_agree {T} :
  forall (C : Cmd T) s1 s2 l,
  sAgree (cmd_fv C) s1 s2 ->
  cmd_acc C s1 l = cmd_acc C s2 l.

Lemma cmd_writes_agree {T} :
  forall (C : Cmd T) s1 s2 l,
    (forall x, cmd_fv C x -> s1 x = s2 x) ->
  cmd_writes C s1 l = cmd_writes C s2 l.

Lemma cmd_acc_plain {T} :
  forall (C : Cmd T) s, cmd_acc (plain C) s = cmd_acc C s.

Lemma cmd_writes_plain {T} :
  forall (C : Cmd T) s,
  cmd_writes (plain C) s = cmd_writes C s.

Operational semantics

Below are the small-step reduction rules of the (standard) operational semantics of programs.

Observe that the process-related commands are ignored and handled as if they were comments, since these are specification-only. Moreover, the transition rules for the parallel composition only allow a program to make a step if the other program is not locked. This allows to model atomic programs using a small-step semantics.

Inductive step : Heap -> Store -> PlainCmd -> Heap -> Store -> PlainCmd -> Prop :=

  | step_seq_l h s C1 h' s' C1' C2 :
    step h s C1 h' s' C1' ->
    step h s (Cseq C1 C2) h' s' (Cseq C1' C2)
  | step_seq_r h s C :
    step h s (Cseq Cskip C) h s C

  | step_assign h s x E :
    let v := expr_eval E s in
    step h s (Cass x E) h (sUpdate s x v) Cskip

  | step_read h s x E v :
    h (expr_eval E s) = Some v ->
    step h s (Cread x E) h (sUpdate s x v) Cskip

  | step_write h s E1 E2 v :
    let l := expr_eval E1 s in
    let v' := expr_eval E2 s in
    h l = Some v ->
    step h s (Cwrite E1 E2) (hUpdate h l (Some v')) s Cskip

  | step_ite_t h s B C1 C2 :
    cond_eval B s = true ->
    step h s (Cite B C1 C2) h s C1
  | step_ite_f h s B C1 C2 :
    cond_eval B s = false ->
    step h s (Cite B C1 C2) h s C2

  | step_while h s B C :
    step h s (Cwhile B C) h s (Cite B (Cseq C (Cwhile B C)) Cskip)

  | step_alloc h s x E l :
    let v := expr_eval E s in
    h l = None ->
    step h s (Calloc x E) (hUpdate h l (Some v)) (sUpdate s x l) Cskip
  | step_dispose h s E :
    let l := expr_eval E s in
    step h s (Cdispose E) (hUpdate h l None) s Cskip

  | step_atom h s C :
    step h s (Catomic C) h s (Cinatom C)
  | step_inatom_l h s C h' s' C' :
    step h s C h' s' C' ->
    step h s (Cinatom C) h' s' (Cinatom C')
  | step_inatom_r h s :
    step h s (Cinatom Cskip) h s Cskip

  | step_par_l h s C1 C2 h' s' C1' :
    step h s C1 h' s' C1' ->
    ~ cmd_locked C2 ->
    step h s (Cpar C1 C2) h' s' (Cpar C1' C2)
  | step_par_r h s C1 C2 h' s' C2' :
    step h s C2 h' s' C2' ->
    ~ cmd_locked C1 ->
    step h s (Cpar C1 C2) h' s' (Cpar C1 C2')
  | step_par_done h s :
    step h s (Cpar Cskip Cskip) h s Cskip

  | step_proc_init h s X P E xs f :
    step h s (Cproc X P E xs f) h s Cskip
  | step_end h s X :
    step h s (Cendproc X) h s Cskip

  | step_act h s X a E C :
    step h s (Cact X a E C) h s (Cinact PMnone C)
  | step_act_l h s C h' s' C' :
    step h s C h' s' C' ->
    step h s (Cinact PMnone C) h' s' (Cinact PMnone C')
  | step_act_r h s :
    step h s (Cinact PMnone Cskip) h s Cskip

  | step_query h s x :
    step h s (Cquery x) h s Cskip.

Add Search Blacklist "step_ind".
Add Search Blacklist "step_sind".

Program basicality, program well-formedness and heap finiteness all remain invariant during program execution.

Lemma step_basic_pres :
  forall C h s C' h' s',
  cmd_basic C -> step h s C h' s' C' -> cmd_basic C'.

Lemma step_wf_pres :
  forall C h s C' h' s',
  cmd_wf C -> step h s C h' s' C' -> cmd_wf C'.

Lemma step_hFinite :
  forall C h s C' h' s',
  step h s C h' s' C' -> hFinite h -> hFinite h'.

The sets of free and modified variables do not grow during program execution.

Lemma step_fv_mod :
  forall C h s C' h' s',
  step h s C h' s' C' ->
    (forall x, cmd_fv C' x -> cmd_fv C x) /\
    (forall x, cmd_mod C' x -> cmd_mod C x) /\
    (forall x, ~ cmd_mod C x -> s x = s' x).

Program execution commutes with store agreement:

Lemma step_agree :
  forall C h s1 s2 C' h' s1' (phi : Var -> Prop),
    (forall x, cmd_fv C x -> phi x) ->
    (sAgree phi s1 s2) ->
    step h s1 C h' s1' C' ->
  exists s2',
    (sAgree phi s1' s2') /\
    step h s2 C h' s2' C'.

A program reduction step always mutates the executed program; one does not end up in the same program after performing a computation step.

Lemma step_neg_C :
forall C h s h' s', ~ step h s C h' s' C.

Fault semantics

The fault semantics of program is defined in terms of the predicate fault h s C and captures whether C is able to fault in a single computation step with respect to heap h and store s.

A fault is defined to be a data-race, a deadlock, or a violation of memory safety.

Any program performs a data-race if two threads access the same shared location, where one of these accesses is a write.

Any parallel program Cpar C1 C2 is deadlocked if C1 and C2 are both locked with respect to cmd_locked.

Moreover, any program is defined to be memory safe if it does not access a shared location has has not been allocated.

Inductive fault {T} : Heap -> Store -> Cmd T -> Prop :=

  | fault_read h s x E :
    h (expr_eval E s) = None -> fault h s (Cread x E)

  | fault_write h s E1 E2 :
    h (expr_eval E1 s) = None -> fault h s (Cwrite E1 E2)

  | fault_alloc h s x E :
    (~ exists l, h l = None) -> fault h s (Calloc x E)
  | fault_dispose h s E :
    h (expr_eval E s) = None -> fault h s (Cdispose E)

  | fault_par_l h s C1 C2 :
    fault h s C1 -> ~ cmd_locked C2 -> fault h s (Cpar C1 C2)
  | fault_par_r h s C1 C2 :
    fault h s C2 -> ~ cmd_locked C1 -> fault h s (Cpar C1 C2)
  | fault_deadlock h s C1 C2 :
    cmd_locked C1 -> cmd_locked C2 -> fault h s (Cpar C1 C2)

  | fault_act h s m C :
    fault h s C -> fault h s (Cinact m C)

  | fault_seq h s C1 C2 :
    fault h s C1 -> fault h s (Cseq C1 C2)

  | fault_atom h s C :
    fault h s C -> fault h s (Cinatom C)

  | fault_race_l h s C1 C2 :
    ~ cmd_locked C1 ->
    ~ cmd_locked C2 ->
    ~ disjoint (cmd_writes C1 s) (cmd_acc C2 s) ->
    fault h s (Cpar C1 C2)
  | fault_race_r h s C1 C2 :
    ~ cmd_locked C1 ->
    ~ cmd_locked C2 ->
    ~ disjoint (cmd_acc C1 s) (cmd_writes C2 s) ->
    fault h s (Cpar C1 C2).

Add Search Blacklist "fault_ind".
Add Search Blacklist "fault_sind".

The fault semantics of programs is closed under store agreement.

Lemma fault_agree {T} :
forall (C : Cmd T) h s1 s2,
sAgree (cmd_fv C) s1 s2 -> fault h s1 C -> fault h s2 C.

The following theorem shows that the operational semantics and fault semantics are coherent, by showing a property of progress: every configuration that does not fault can either make a computation step or has already terminated.

Theorem step_progress :
forall C h s,
~ fault h s C -> C = Cskip \/ exists C' h' s', step h s C h' s' C'.

Ghost operational semantics

The ghost operational semantics of (ghost) programs is the lock-step execution of the (ordinary) operational semantics of programs and the execution of all its process-algebraic models.

Ghost commands are programs that maintain some extra metadata. In particular, every partially executed action program holds (1) the corresponding process identifier, (2) the action that is being executed, and (3) a snapshot of the heap made when the action block started to be executed.

Inductive GhostMetadata :=
  | GMdata(pid : Val)(a : Act)(v : Val)(hs : Heap).

Add Search Blacklist "GhostMetadata_rect".
Add Search Blacklist "GhostMetadata_ind".
Add Search Blacklist "GhostMetadata_rec".
Add Search Blacklist "GhostMetadata_sind".

Definition GhostCmd : Type := Cmd GhostMetadata.

Inductive gstep : Heap -> ProcMap -> Store -> Store -> GhostCmd ->
                  Heap -> ProcMap -> Store -> Store -> GhostCmd -> Prop :=

  | gstep_seq_l h pm s g C :
    gstep h pm s g (Cseq Cskip C) h pm s g C
  | gstep_seq_r h pm s g C1 C2 h' pm' s' g' C1' :
    gstep h pm s g C1 h' pm' s' g' C1' ->
    gstep h pm s g (Cseq C1 C2) h' pm' s' g' (Cseq C1' C2)

  | gstep_assign h pm s g x E :
    let v := expr_eval E s in
    gstep h pm s g (Cass x E) h pm (sUpdate s x v) g Cskip

  | gstep_read h pm s g x E v :
    h (expr_eval E s) = Some v ->
    gstep h pm s g (Cread x E) h pm (sUpdate s x v) g Cskip

  | gstep_write h pm s g E1 E2 v :
    let l := expr_eval E1 s in
    let v' := expr_eval E2 s in
    h l = Some v ->
    gstep h pm s g (Cwrite E1 E2) (hUpdate h l (Some v')) pm s g Cskip

  | gstep_ite_t h pm s g B C1 C2 :
    cond_eval B s = true ->
    gstep h pm s g (Cite B C1 C2) h pm s g C1
  | gstep_ite_f h pm s g B C1 C2 :
    cond_eval B s = false ->
    gstep h pm s g (Cite B C1 C2) h pm s g C2

  | gstep_while h pm s g B C :
    gstep h pm s g (Cwhile B C) h pm s g (Cite B (Cseq C (Cwhile B C)) Cskip)

  | gstep_alloc h pm s g x E l :
    let v : Val := expr_eval E s in
    h l = None ->
    gstep h pm s g (Calloc x E) (hUpdate h l (Some v)) pm (sUpdate s x l) g Cskip
  | gstep_dispose h pm s g E :
    let l := expr_eval E s in
    gstep h pm s g (Cdispose E) (hUpdate h l None) pm s g Cskip

  | gstep_atom h pm s g C :
    gstep h pm s g (Catomic C) h pm s g (Cinatom C)
  | gstep_inatom_l h pm s g C h' pm' s' g' C' :
    gstep h pm s g C h' pm' s' g' C' ->
    gstep h pm s g (Cinatom C) h' pm' s' g' (Cinatom C')
  | gstep_inatom_r h pm s g :
    gstep h pm s g (Cinatom Cskip) h pm s g Cskip

  | gstep_par_l h pm s g C1 C2 h' pm' s' g' C1' :
    gstep h pm s g C1 h' pm' s' g' C1' ->
    ~ cmd_locked C2 ->
    gstep h pm s g (Cpar C1 C2) h' pm' s' g' (Cpar C1' C2)
  | gstep_par_r h pm s g C1 C2 h' pm' s' g' C2' :
    gstep h pm s g C2 h' pm' s' g' C2' ->
    ~ cmd_locked C1 ->
    gstep h pm s g (Cpar C1 C2) h' pm' s' g' (Cpar C1 C2')
  | gstep_par_done h pm s g :
    gstep h pm s g (Cpar Cskip Cskip) h pm s g Cskip

  | gstep_proc_init h pm s g x Pf E xs f pid :
    pm pid = PEfree ->
    let HP := Pf E in
    let P := pDehybridise HP s in
    let f' := expr_eval_map f s in
    gstep h pm s g (Cproc x Pf E xs f) h (pmUpdate pm pid (PEelem perm_full P xs f')) s (sUpdate g x pid) Cskip
  | gstep_proc_end h pm s g x P xs f :
    let pid := g x in
    pmeBisim (pm pid) (PEelem perm_full P xs f) ->
    pterm P ->
    gstep h pm s g (Cendproc x) h (pmUpdate pm pid PEfree) s g Cskip

  | gstep_act h pm s g x a E C :
    let v := expr_eval E s in
    let m := GMdata (g x) a v h in
    gstep h pm s g (Cact x a E C) h pm s g (Cinact m C)
  | gstep_act_l h pm s g m C h' pm' s' g' C' :
    gstep h pm s g C h' pm' s' g' C' ->
    gstep h pm s g (Cinact m C) h' pm' s' g' (Cinact m C')
  | gstep_act_r h pm s g pid a v hs q P P' xs f ps1 ps2 :
    pmeBisim (pm pid) (PEelem q P xs f) ->
      (forall x, In x xs -> hs (f x) = Some (ps1 x)) ->
      (forall x, In x xs -> h (f x) = Some (ps2 x)) ->
    pstep P ps1 (PLact a v) P' ps2 ->
    let pm' := pmUpdate pm pid (PEelem q P' xs f) in
    gstep h pm s g (Cinact (GMdata pid a v hs) Cskip) h pm' s g Cskip

  | gstep_query g x pm q P xs f ps P' s h :
    let pid := g x in
    pmeBisim (pm pid) (PEelem q P xs f) ->
    (forall x, In x xs -> h (f x) = Some (ps x)) ->
    pstep P ps PLassert P' ps ->
    let pm' := pmUpdate pm pid (PEelem q P' xs f) in
    gstep h pm s g (Cquery x) h pm' s g Cskip.

Add Search Blacklist "gstep_ind".
Add Search Blacklist "gstep_sind".

The reduction rules of the standard operational semantics are embedded in the reduction rules of the ghost operational semantics, as is shown by the following theorem.

Theorem gstep_sim :
  forall C h pm s g C' h' pm' s' g',
  gstep h pm s g C h' pm' s' g' C' ->
  step h s (plain C) h' s' (plain C').

Moreover, the ghost operational semantics can mimick the steps of the standard operational semantics for any basic program.

Theorem step_basic_sim :
  forall C h pm s g C' h' s',
  cmd_basic C ->
  step h s (plain C) h' s' C' ->
  exists C'', gstep h pm s g C h' pm s' g C'' /\ C' = plain C''.

Program basicality, well-formedness and process map finiteness all remain invariant during ghost program execution.

Lemma gstep_basic_pres :
  forall C h pm s g C' h' pm' s' g',
  gstep h pm s g C h' pm' s' g' C' ->
  cmd_basic C ->
  cmd_basic C'.

Lemma gstep_wf_pres :
  forall C h pm s g C' h' pm' s' g',
  gstep h pm s g C h' pm' s' g' C' ->
  cmd_wf C ->
  cmd_wf C'.

Lemma gstep_pmFinite_pres :
  forall C h pm s g C' h' pm' s' g',
  gstep h pm s g C h' pm' s' g' C' ->
  pmFinite pm ->
  pmFinite pm'.

The ghost semantics can simulate computation steps made with bisimilar process maps.

Lemma gstep_procmap_eq :
  forall C h pm1 pm2 s g C' h' pm1' s' g',
    pmBisim pm1 pm2 ->
    gstep h pm1 s g C h' pm1' s' g' C' ->
  exists pm2',
    gstep h pm2 s g C h' pm2' s' g' C' /\
    pmBisim pm1' pm2'.

The sets of free and modified variables do not grow during program ghost execution.

Lemma gstep_fv_mod_g :
  forall C h pm s g C' h' pm' s' g' x,
  gstep h pm s g C h' pm' s' g' C' ->
  ~ cmd_mod C x -> g x = g' x.

Lemma gstep_fv_mod :
  forall C h pm s g C' h' pm' s' g',
  gstep h pm s g C h' pm' s' g' C' ->
    (forall x, cmd_fv C' x -> cmd_fv C x) /\
    (forall x, cmd_mod C' x -> cmd_mod C x) /\
    (forall x, ~ cmd_mod C x -> s x = s' x) /\
    (forall x, ~ cmd_mod C x -> g x = g' x).

Program ghost execution commutes with store agreement.

Lemma gstep_agree :
  forall C h pm s1 s2 g C' h' pm' s1' g' (phi : Var -> Prop),
    (forall x, cmd_fv C x -> phi x) ->
    (forall x, phi x -> s1 x = s2 x) ->
    gstep h pm s1 g C h' pm' s1' g' C' ->
  exists s2',
    (forall x, phi x -> s1' x = s2' x) /\
    gstep h pm s2 g C h' pm' s2' g' C'.

Lemma gstep_agree_g :
  forall C h pm s g1 g2 C' h' pm' s' g1' (phi : Var -> Prop),
    (forall x, cmd_fv C x -> phi x) ->
    (forall x, phi x -> g1 x = g2 x) ->
    gstep h pm s g1 C h' pm' s' g1' C' ->
  exists g2',
    (forall x, phi x -> g1' x = g2' x) /\
    gstep h pm s g2 C h' pm' s' g2' C'.

The following lemma is for later convenience.

Lemma gstep_agree_sim :
  forall C h pm s1 s2 g C' h' pm' s1' s2' g',
    (forall x, cmd_fv C x -> s1 x = s2 x) ->
    (forall x, cmd_fv C x -> s1' x = s2' x) ->
  step h s1 (plain C) h' s1' (plain C') ->
  gstep h pm s2 g C h' pm' s2' g' C' ->
  gstep h pm s1 g C h' pm' s1' g' C'.

Ghost steps in basic programs do not affect the ghost components pm and g.

Lemma gstep_basic_ghostdata_pres :
  forall C h pm s g C' h' pm' s' g',
  cmd_basic C ->
  gstep h pm s g C h' pm' s' g' C' ->
  pm = pm' /\ g = g'.

Ghost fault semantics

The ghost fault semantics defines the notions of data-races and memory-safety, likewise to fault, as well as all necessary conditions for a configuration in the ghost semantics to make progress (see gstep_progress for the proof).

Inductive gfault : Heap -> ProcMap -> Store -> Store -> GhostCmd -> Prop :=

  | gfault_read h pm s g x E :
    h (expr_eval E s) = None ->
    gfault h pm s g (Cread x E)

  | gfault_write h pm s g E1 E2 :
    h (expr_eval E1 s) = None ->
    gfault h pm s g (Cwrite E1 E2)

  | gfault_alloc h pm s g x E :
    (~ exists l, h l = None) ->
    gfault h pm s g (Calloc x E)

  | gfault_dispose h pm s g E :
    h (expr_eval E s) = None ->
    gfault h pm s g (Cdispose E)

  | gfault_seq h pm s g C1 C2 :
    gfault h pm s g C1 ->
    gfault h pm s g (Cseq C1 C2)

  | gfault_atom h pm s g C :
    gfault h pm s g C ->
    gfault h pm s g (Cinatom C)

  | gfault_par_l h pm s g C1 C2 :
    gfault h pm s g C1 ->
    ~ cmd_locked C2 ->
    gfault h pm s g (Cpar C1 C2)
  | gfault_par_r h pm s g C1 C2 :
    gfault h pm s g C2 ->
    ~ cmd_locked C1 ->
    gfault h pm s g (Cpar C1 C2)
  | gfault_par_deadlock h pm s g C1 C2 :
    cmd_locked C1 ->
    cmd_locked C2 ->
    gfault h pm s g (Cpar C1 C2)

  | gfault_act_step h pm s g m C :
    gfault h pm s g C ->
    gfault h pm s g (Cinact m C)
  | gfault_act_end_1 h pm s g pid a v hs :
    (~ pmeOcc (pm pid)) ->
    gfault h pm s g (Cinact (GMdata pid a v hs) Cskip)
  | gfault_act_end_2 h pm s g pid a v hs q P xs f :
    pmeBisim (pm pid) (PEelem q P xs f) ->
    (exists x, In x xs /\ hs (f x) = None) ->
    gfault h pm s g (Cinact (GMdata pid a v hs) Cskip)
  | gfault_act_end_3 h pm s g pid a v hs q P xs f :
    pmeBisim (pm pid) (PEelem q P xs f) ->
    (exists x, In x xs /\ h (f x) = None) ->
    gfault h pm s g (Cinact (GMdata pid a v hs) Cskip)
  | gfault_act_end_4 h pm s g pid a v hs q P xs f ps1 ps2 :
    pmeBisim (pm pid) (PEelem q P xs f) ->
      (forall x, In x xs -> hs (f x) = Some (ps1 x)) ->
      (forall x, In x xs -> h (f x) = Some (ps2 x)) ->
      (~ exists P', pstep P ps1 (PLact a v) P' ps2) ->
    gfault h pm s g (Cinact (GMdata pid a v hs) Cskip)

  | gfault_proc_init h pm s g x P E xs f :
    (~ exists pid, pm pid = PEfree) ->
    gfault h pm s g (Cproc x P E xs f)
  | gfault_proc_end_1 h pm s g x :
    ~ pmeEntire (pm (g x)) ->
    gfault h pm s g (Cendproc x)
  | gfault_proc_end_2 h pm s g x P xs f :
    pmeBisim (pm (g x)) (PEelem perm_full P xs f) ->
    ~ pterm P ->
    gfault h pm s g (Cendproc x)

  | gfault_query_1 h pm s g x :
    let pid := g x in
    (~ pmeOcc (pm pid)) ->
    gfault h pm s g (Cquery x)
  | gfault_query_2 h pm s g x q P xs f :
    let pid := g x in
    pmeBisim (pm pid) (PEelem q P xs f) ->
    (exists y, In y xs /\ h (f y) = None) ->
    gfault h pm s g (Cquery x)
  | gfault_query_3 h pm s g x q P xs f ps :
    let pid := g x in
    pmeBisim (pm pid) (PEelem q P xs f) ->
      (forall x, In x xs -> h (f x) = Some (ps x)) ->
      (~ exists P', pstep P ps (PLassert) P' ps) ->
    gfault h pm s g (Cquery x)

  | gfault_race_l h pm s g C1 C2 :
    ~ cmd_locked C1 ->
    ~ cmd_locked C2 ->
    ~ disjoint (cmd_writes C1 s) (cmd_acc C2 s) ->
    gfault h pm s g (Cpar C1 C2)
  | gfault_race_r h pm s g C1 C2 :
    ~ cmd_locked C1 ->
    ~ cmd_locked C2 ->
    ~ disjoint (cmd_acc C1 s) (cmd_writes C2 s) ->
    gfault h pm s g (Cpar C1 C2).

Add Search Blacklist "gfault_ind".
Add Search Blacklist "gfault_sind".

The program fault semantics is embedded in the ghost fault semantics.

Theorem fault_emb :
  forall C h pm s g,
  fault h s (plain C) ->
  gfault h pm s g C.

The following theorem shows that ghost reduction steps are progressive for non-faulty programs. Being progressive means that any ghost configuration that does not fault has either terminated or can make another computation step.

Lemma heap_procvar_cover :
  forall (xs : list ProcVar)(h : Heap)(f : ProcVar -> Val),
    (forall x, In x xs -> h (f x) <> None) ->
  exists g : ProcVar -> Val,
    forall x, In x xs -> h (f x) = Some (g x).

Theorem gstep_progress :
  forall C h pm s g,
  ~ gfault h pm s g C ->
  C = Cskip \/ exists C' h' pm' s' g', gstep h pm s g C h' pm' s' g' C'.

The faulting of ghost programs is stable under replacement of process maps with bisimilar ones, as well as replacement of (ghost) stores with stores that agree on all variables occuring freely in the program.

Lemma gfault_pmBisim :
  forall C h pm1 pm2 s g,
  pmBisim pm1 pm2 -> gfault h pm1 s g C -> gfault h pm2 s g C.

Add Parametric Morphism : gfault
  with signature eq ==> pmBisim ==> eq ==> eq ==> eq ==> iff
    as gfault_pmBisim_mor.

Ghost faults are dependent on variables occuring freely inside programs.

Lemma gfault_agree :
  forall C h pm s1 s2 g,
  sAgree (cmd_fv C) s1 s2 -> gfault h pm s1 g C -> gfault h pm s2 g C.

Lemma gfault_agree_g :
  forall C h pm s g1 g2,
  sAgree (cmd_fv C) g1 g2 -> gfault h pm s g1 C -> gfault h pm s g2 C.

End Programs.