Theory Lang

theory Lang
imports Main VHelper
begin

This file defines the syntax and semantics of the programming language used by O'Hearn and Brookes. For simplicity, we do not allow resource-owned variables.

(Adapted to Isabelle 2016-1 by Qin Yu and James Brotherston)

Language syntax and semantics

We define the syntax and the operational semantics of the programming language of O'Hearn and Brookes.

type_synonym var = string — Variables
type_synonym rname = string — Resource names
type_synonym heap = (nat ⇀ nat) — Heaps
type_synonym stack = (var ⇒ nat) — Stacks
type_synonym state = stack × heap — States

datatype exp = — Arithmetic expressions
    Evar var — Variable
  | Enum nat — Constant
  | Eplus exp exp — Addition

datatype bexp = — Boolean expressions
    Beq exp exp — Equality of expressions
  | Band bexp bexp — Conjunction
  | Bnot bexp — Negation

datatype cmd = — Commands
    Cskip — Empty command
  | Cassign var exp — Assignment
  | Cread var exp — Memory load
  | Cwrite exp exp — Memory store
  | Calloc var exp — Memory allocation
  | Cdispose exp — Memory de-allocation
  | Cseq cmd cmd — Sequential composition
  | Cpar cmd cmd — Parallel composition
  | Cif bexp cmd cmd — If-then-else
  | Cwhile bexp cmd — While loops
  | Clocal var exp cmd — Local variable declaration
  | Cinlocal var nat cmd — Local variable declaration (runtime)
  | Cresource rname cmd — Resource declaration
  | Cwith rname bexp cmd — Conditional critical region
  | Cinwith rname cmd — Conditional critical region (runtime)

Arithmetic expressions (exp) consist of variables, constants, and arithmetic operations. Boolean expressions (bexp) consist of comparisons between arithmetic expressions. Commands (cmd) include the empty command, variable assignments, memory reads, writes, allocations and deallocations, sequential and parallel composition, conditionals, while loops, local variable declarations, resource declarations and conditional critical regions (CCRs). There are two command forms (Cinlocal, Cinwith) that represent partially executed local variable declarations and CCRs and do not appear in user programs. This restriction is captured by the following definition:

The following function returns the set of locks that a command is currently holding.

primrec
  locked :: cmd ⇒ rname set
where
    locked Cskip = {}
  | locked (Cassign x E) = {}
  | locked (Cread x E) = {}
  | locked (Cwrite E E') = {}
  | locked (Calloc x E) = {}
  | locked (Cdispose E) = {}
  | locked (Cseq C1 C2) = (locked C1)
  | locked (Cpar C1 C2) = (locked C1 ∪ locked C2)
  | locked (Cif B C1 C2) = {}
  | locked (Cwhile B C) = {}
  | locked (Clocal x E C) = {}
  | locked (Cinlocal x v C) = (locked C)
  | locked (Cresource r C) = (locked C - {r})
  | locked (Cwith r B C) = {}
  | locked (Cinwith r C) = ({r} ∪ locked C)

Now the same definition, but return a list of locks that the command is currently holding in some fixed order. This defnition is needed to work around the deep embedding of assertions.

locked C = set (llocked C)

by (induct C, simp_all)

Semantics of expressions

Denotational semantics for arithmetic and boolean expressions.

primrec
  edenot :: exp ⇒ stack ⇒ nat
where
    edenot (Evar v) s = s v
  | edenot (Enum n) s = n
  | edenot (Eplus e1 e2) s = edenot e1 s + edenot e2 s

primrec
  bdenot :: bexp ⇒ stack ⇒ bool
where
    bdenot (Beq e1 e2) s = (edenot e1 s = edenot e2 s)
  | bdenot (Band b1 b2) s = (bdenot b1 s ∧ bdenot b2 s)
  | bdenot (Bnot b) s = (¬ bdenot b s)

Semantics of commands

We give a standard small-step operational semantics to commands with configurations being command-state pairs.

For illustration purposes, our semantics for Cwrite E E' is unusual in that if E is not allocated, then the command will allocate E and do the assignment. Requiring that (edenot E s) ∈ dom h does not change the proof.

inductive
red :: cmd ⇒ state ⇒ cmd ⇒ state ⇒ bool
where

red_Seq1[intro]:

red (Cseq Cskip C) σ C σ

red_Seq2[elim]:

red C1 σ C1' σ'

red (Cseq C1 C2) σ (Cseq C1' C2) σ'

red_If1[intro]:

bdenot B (fst σ)

red (Cif B C1 C2) σ C1 σ

red_If2[intro]:

¬ bdenot B (fst σ)

red (Cif B C1 C2) σ C2 σ

red_Par1[elim]:

red C1 σ C1' σ'; disjoint (locked C1') (locked C2)

red (Cpar C1 C2) σ (Cpar C1' C2) σ'

red_Par2[elim]:

red C2 σ C2' σ'; disjoint (locked C1) (locked C2')

red (Cpar C1 C2) σ (Cpar C1 C2') σ'

red_Par3[intro]:

red (Cpar Cskip Cskip) σ (Cskip) σ

red_Loop[intro]:

red (Cwhile B C) σ (Cif B (Cseq C (Cwhile B C)) Cskip) σ

red_Local1[intro]:

v = edenot E (fst σ)

red (Clocal x E C) σ (Cinlocal x v C) σ

red_Local2[intro]:

σ = (s,h); red C (s(x:=v),h) C' (s',h'); v' = s' x; σ' = (s'(x := s x), h')

red (Cinlocal x v C) σ (Cinlocal x v' C') σ'

red_Local3[intro]:

red (Cinlocal x v Cskip) σ Cskip σ

red_Res1[intro]:

red C σ C' σ'

red (Cresource r C) σ (Cresource r C') σ'

red_Res2[intro]:

red (Cresource r Cskip) σ Cskip σ

red_With1[intro]:

bdenot B (fst σ)

red (Cwith r B C) σ (Cinwith r C) σ

red_With2[elim]:

red C σ C' σ'; r ∉ locked C'

red (Cinwith r C) σ (Cinwith r C') σ'

red_With3[intro]:

red (Cinwith r Cskip) σ Cskip σ

red_Assign[intro]:

σ = (s,h); σ' = (s(x := edenot E s), h)

red (Cassign x E) σ Cskip σ'

red_Read[intro]:

σ = (s,h); h(edenot E s) = Some v; σ' = (s(x := v), h)

red (Cread x E) σ Cskip σ'

red_Write[intro]:

σ = (s,h); σ' = (s, h(edenot E s ↦ edenot E' s))

red (Cwrite E E') σ Cskip σ'

red_Alloc[intro]:

σ = (s,h); v ∉ dom h; σ' = (s(x := v), h(v ↦ edenot E s))

red (Calloc x E) σ Cskip σ'

red_Free[intro]:

σ = (s,h); σ' = (s, h(edenot E s := None))

red (Cdispose E) σ Cskip σ'

inductive_cases red_par_cases: red (Cpar C1 C2) σ C' σ'

Abort semantics

Below, we define the sets of memory accesses and memory writes that a command performs in one step. These are used to define what a race condition is. We do not count memory allocation as a memory access because the memory cell allocated is fresh.

primrec
  accesses :: cmd ⇒ stack ⇒ nat set
where
    accesses Cskip s = {}
  | accesses (Cassign x E) s = {}
  | accesses (Cread x E) s = {edenot E s}
  | accesses (Cwrite E E') s = {edenot E s}
  | accesses (Calloc x E) s = {}
  | accesses (Cdispose E) s = {edenot E s}
  | accesses (Cseq C1 C2) s = accesses C1 s
  | accesses (Cpar C1 C2) s = accesses C1 s ∪ accesses C2 s
  | accesses (Cif B C1 C2) s = {}
  | accesses (Cwhile B C) s = {}
  | accesses (Clocal x E C) s = {}
  | accesses (Cinlocal x v C) s = accesses C (s(x:=v))
  | accesses (Cresource r C) s = accesses C s
  | accesses (Cwith r B C) s = {}
  | accesses (Cinwith r C) s = accesses C s

primrec
  writes :: cmd ⇒ stack ⇒ nat set
where
    writes Cskip s = {}
  | writes (Cassign x E) s = {}
  | writes (Cread x E) s = {}
  | writes (Cwrite E E') s = {edenot E s}
  | writes (Calloc x E) s = {}
  | writes (Cdispose E) s = {edenot E s}
  | writes (Cseq C1 C2) s = writes C1 s
  | writes (Cpar C1 C2) s = writes C1 s ∪ writes C2 s
  | writes (Cif B C1 C2) s = {}
  | writes (Clocal x E C) s = {}
  | writes (Cinlocal x v C) s = writes C (s(x:=v))
  | writes (Cwhile B C) s = {}
  | writes (Cresource r C) s = writes C s
  | writes (Cwith r B C) s = {}
  | writes (Cinwith r C) s = writes C s

A command aborts in a given state whenever it can access unallocated memory or has a race condition in its first execution step. The soundness statement of the logic asserts that these transitions never occur.

inductive
aborts :: cmd ⇒ state ⇒ bool
where

aborts_Seq[intro]:

aborts C1 σ

aborts (Cseq C1 C2) σ

aborts_Par1[intro]:

aborts C1 σ

aborts (Cpar C1 C2) σ

aborts_Par2[intro]:

aborts C2 σ

aborts (Cpar C1 C2) σ

aborts_Race1[intro]:

¬ disjoint (accesses C1 (fst σ)) (writes C2 (fst σ))

aborts (Cpar C1 C2) σ

aborts_Race2[intro]:

¬ disjoint (writes C1 (fst σ)) (accesses C2 (fst σ))

aborts (Cpar C1 C2) σ

aborts_Local[intro]:

aborts C ((fst σ)(x:=v), snd σ)

aborts (Cinlocal x v C) σ

aborts_Res[intro]:

aborts C σ

aborts (Cresource r C) σ

aborts_With[intro]:

aborts C σ

aborts (Cinwith r C) σ

aborts_Read[intro]:

edenot E (fst σ) ∉ dom (snd σ)

aborts (Cread x E) σ

aborts_Write[intro]:

edenot E (fst σ) ∉ dom (snd σ)

aborts (Cwrite E E') σ

aborts_Free[intro]:

edenot E (fst σ) ∉ dom (snd σ)

aborts (Cdispose E) σ

Well-formed commands

Well-formed commands are those that can arise from a user command by a reduction sequence. In particular, they can have partially executed CCRs only at reduction positions and their partially executed CCRs must satisfy mutual exclusion.

Now, we establish some basic properties of well-formed commands:

(1) User commands are well-formed and have no locks acquired.

lemma user_cmdD:

user_cmd C

(wf_cmd C ∧ locked C = {})

by (induct C, auto)

corollary user_cmd_wf[intro]:

user_cmd C

wf_cmd C

by (drule user_cmdD, simp)

corollary user_cmd_llocked[simp]:

user_cmd C

llocked C = []

by (drule user_cmdD, simp add: locked_eq)

(2) Well-formedness is preserved under reduction.

lemma red_wf_cmd:

red C σ C' σ' ; wf_cmd C

wf_cmd C'

by (subgoal_tac wf_cmd C ⟶ wf_cmd C', erule_tac[2] red.induct, auto dest: user_cmdD)

(3) Well-formed commands satisfy mutual-exclusion.

lemma wf_cmd_distinct_locked:

wf_cmd C

distinct (llocked C)

by (induct C, auto simp add: distinct_removeAll locked_eq disjoint_def)

Free variables, updated variables and substitutions

The free variables of expressions, boolean expressions, and commands are defined as expected:

primrec
  fvE :: exp ⇒ var set
where
  fvE (Evar v) = {v}
| fvE (Enum n) = {}
| fvE (Eplus e1 e2) = (fvE e1 ∪ fvE e2)

primrec
  fvB :: bexp ⇒ var set
where
  fvB (Beq e1 e2) = (fvE e1 ∪ fvE e2)
| fvB (Band b1 b2) = (fvB b1 ∪ fvB b2)
| fvB (Bnot b) = (fvB b)

primrec
  fvC :: cmd ⇒ var set
where
  fvC (Cskip) = {}
| fvC (Cassign v E) = ({v} ∪ fvE E)
| fvC (Cread v E) = ({v} ∪ fvE E)
| fvC (Cwrite E1 E2) = (fvE E1 ∪ fvE E2)
| fvC (Calloc v E) = ({v} ∪ fvE E)
| fvC (Cdispose E) = (fvE E)
| fvC (Cseq C1 C2) = (fvC C1 ∪ fvC C2)
| fvC (Cpar C1 C2) = (fvC C1 ∪ fvC C2)
| fvC (Cif B C1 C2) = (fvB B ∪ fvC C1 ∪ fvC C2)
| fvC (Cwhile B C) = (fvB B ∪ fvC C)
| fvC (Clocal x E C) = (fvE E ∪ (fvC C - {x}))
| fvC (Cinlocal x v C)= (fvC C - {x})
| fvC (Cresource r C) = (fvC C)
| fvC (Cwith r B C) = (fvB B ∪ fvC C)
| fvC (Cinwith r C) = (fvC C)

Below, we define the set of syntactically updated variables of a command. This set overapproximates the set of variables that are actually updated during the command's execution.

primrec
wrC :: cmd ⇒ var set
where
wrC (Cskip) = {}
| wrC (Cassign v E) = {v}
| wrC (Cread v E) = {v}
| wrC (Cwrite E1 E2) = {}
| wrC (Calloc v E) = {v}
| wrC (Cdispose E) = {}
| wrC (Cseq C1 C2) = (wrC C1 ∪ wrC C2)
| wrC (Cpar C1 C2) = (wrC C1 ∪ wrC C2)
| wrC (Cif B C1 C2) = (wrC C1 ∪ wrC C2)
| wrC (Cwhile B C) = (wrC C)
| wrC (Clocal x E C) = (wrC C - {x})
| wrC (Cinlocal x v C)= (wrC C - {x})
| wrC (Cresource r C) = (wrC C)
| wrC (Cwith r B C) = (wrC C)
| wrC (Cinwith r C) = (wrC C)

We also define the operation of substituting an expression for a variable in expressions.

primrec
  subE :: var ⇒ exp ⇒ exp ⇒ exp
where
  subE x E (Evar y) = (if x = y then E else Evar y)
| subE x E (Enum n) = Enum n
| subE x E (Eplus e1 e2) = Eplus (subE x E e1) (subE x E e2)

primrec
  subB :: var ⇒ exp ⇒ bexp ⇒ bexp
where
  subB x E (Beq e1 e2) = Beq (subE x E e1) (subE x E e2)
| subB x E (Band b1 b2) = Band (subB x E b1) (subB x E b2)
| subB x E (Bnot b) = Bnot (subB x E b)

Basic properties of substitutions:

lemma subE_assign:

edenot (subE x E e) s = edenot e (s(x := edenot E s))

by (induct e, simp_all)

lemma subB_assign:

bdenot (subB x E b) s = bdenot b (s(x := edenot E s))

by (induct b, simp_all add: subE_assign fun_upd_def)

Variable erasure

The following function erases all assignments and reads to variables in the set X.

primrec
  rem_vars :: var set ⇒ cmd ⇒ cmd
where
    rem_vars X Cskip = Cskip
  | rem_vars X (Cassign x E) = (if x ∈ X then Cseq Cskip Cskip else Cassign x E)
  | rem_vars X (Cread x E) = (if x ∈ X then Cseq Cskip Cskip else Cread x E)
  | rem_vars X (Cwrite E E') = Cwrite E E'
  | rem_vars X (Calloc x E) = Calloc x E
  | rem_vars X (Cdispose E) = Cdispose E
  | rem_vars X (Cseq C1 C2) = Cseq (rem_vars X C1) (rem_vars X C2)
  | rem_vars X (Cpar C1 C2) = Cpar (rem_vars X C1) (rem_vars X C2)
  | rem_vars X (Cif B C1 C2) = Cif B (rem_vars X C1) (rem_vars X C2)
  | rem_vars X (Cwhile B C) = Cwhile B (rem_vars X C)
  | rem_vars X (Clocal x E C) = Clocal x E (rem_vars (X - {x}) C)
  | rem_vars X (Cinlocal x v C) = Cinlocal x v (rem_vars (X - {x}) C)
  | rem_vars X (Cresource r C) = Cresource r (rem_vars X C)
  | rem_vars X (Cwith r B C) = Cwith r B (rem_vars X C)
  | rem_vars X (Cinwith r C) = Cinwith r (rem_vars X C)

Properties of variable erasure:

lemma remvars_simps[simp]:

locked (rem_vars X C) = locked C

llocked (rem_vars X C) = llocked C

user_cmd (rem_vars X C) = user_cmd C

rem_vars X (rem_vars X C) = rem_vars X C

by (induct C arbitrary: X, simp_all)+

lemma accesses_remvars:

accesses (rem_vars X C) s ⊆ accesses C s

by (induct C arbitrary: X s, simp_all, fast)

lemma writes_remvars[simp]:

writes (rem_vars X C) = writes C

by (rule ext, induct C arbitrary: X, simp_all)

lemma skip_simps[simp]:

¬ red Cskip σ C' σ'

¬ aborts Cskip σ

(rem_vars X C = Cskip) ⟷ (C = Cskip)

(Cskip = rem_vars X C) ⟷ (C = Cskip)

by (auto elim: aborts.cases red.cases)
(induct C, auto split: if_split_asm)+

lemma disjoint_minus:

disjoint (X - Z) Y = disjoint X (Y - Z)

by (auto simp add: disjoint_def)

lemma aux_red[rule_format]:
red C σ C' σ' ⟹ ∀X C1. C = rem_vars X C1 ⟶ disjoint X (fvC C) ⟶ ¬ aborts C1 σ ⟶
(∃C2 s2. red C1 σ C2 (s2,snd σ') ∧ rem_vars X C2 = C' ∧ agrees (-X) (fst σ') s2)
apply (erule_tac red.induct, simp_all, tactic {* ALLGOALS (clarify_tac @{context}) *})
apply (case_tac C1, simp_all split: if_split_asm, (fastforce simp add: agrees_def)+)
apply (case_tac[1-5] C1a, simp_all split: if_split_asm, (fastforce intro: agrees_refl)+)
apply (case_tac[!] C1, simp_all split: if_split_asm)
apply (tactic {* TRYALL (clarify_tac @{context}) *}, simp_all add: disjoint_minus [THEN sym])
apply (fastforce simp add: agrees_def)+
apply (intro exI conjI, rule_tac v=v in red_Alloc, (fastforce simp add: agrees_def)+)
done

lemma aborts_remvars:

aborts (rem_vars X C) σ

aborts C σ

apply (induct C arbitrary: X σ, erule_tac[!] aborts.cases, simp_all split: if_split_asm)
apply (tactic {* TRYALL (fast_tac @{context}) *})
apply (clarsimp, rule, erule contrapos_nn, simp, erule disjoint_search, rule accesses_remvars)+
done

Basic properties of the semantics

lemma writes_accesses:

writes C s ⊆ accesses C s

by (induct C arbitrary: s, auto)

Proposition 4.1: Properties of basic properties of red.

lemma red_properties:

red C σ C' σ'

fvC C' ⊆ fvC C
∧ wrC C' ⊆ wrC C
∧ agrees (- wrC C) (fst σ') (fst σ)

by (erule red.induct, auto simp add: agrees_def)

Proposition 4.2: Semantics does not depend on variables not free in the term

lemma exp_agrees:

agrees (fvE E) s s'

edenot E s = edenot E s'

by (simp add: agrees_def, induct E, auto)

lemma bexp_agrees:

agrees (fvB B) s s'

bdenot B s = bdenot B s'

by (induct B, auto simp add: exp_agrees)

lemma accesses_agrees:

agrees (fvC C) s s'

accesses C s = accesses C s'

apply (induct C arbitrary: s s', simp_all add: exp_agrees, clarsimp)
apply (erule mall2_impD, simp add: agrees_def)
done

lemma writes_agrees:

agrees (fvC C) s s'

writes C s = writes C s'

apply (induct C arbitrary: s s', simp_all add: exp_agrees, clarsimp)
apply (erule mall2_impD, simp add: agrees_def)
done

lemma red_agrees[rule_format]:
  red C σ C' σ' ⟹ ∀X s. agrees X (fst σ) s ⟶ snd σ = h ⟶ fvC C ⊆ X ⟶
   (∃s' h'. red C (s, h) C' (s', h') ∧ agrees X (fst σ') s' ∧ snd σ' = h')
apply (erule red.induct, simp_all)
apply (tactic {* TRYALL (fast_tac @{context}) *}, auto)
apply (rule, rule conjI, rule red_If1, simp, subst bexp_agrees, fast+)
apply (rule, rule conjI, rule red_If2, simp, subst bexp_agrees, fast+)
apply (rule, rule conjI, rule, simp, subst exp_agrees, fast+)
apply (drule_tac a=X ∪ {x} and b=sa(x:=v) in all2_imp2D, fastforce simp add: agrees_def, fast)
apply (clarsimp, rule, rule conjI, rule, fast+, fastforce simp add: agrees_def)
apply (rule, rule conjI, rule, simp, subst bexp_agrees, fast+)
apply (rule, rule, rule, fast, simp_all, subst exp_agrees, fast)
apply (clarsimp simp add: agrees_def)
apply (rule, rule, rule, fast, simp_all, subst exp_agrees, fast, fast)
apply (clarsimp simp add: agrees_def)
apply (rule, rule, rule, fast, simp_all, subst exp_agrees, fast, clarsimp?)
apply (rule ext, clarsimp, fast intro: exp_agrees)
apply (rule, rule, rule_tac v=v in red_Alloc, simp_all, fast, auto)
apply (rule ext, clarsimp, fast intro: exp_agrees)
apply (clarsimp simp add: agrees_def)
apply (auto)
apply (rule, rule, rule, fast, simp_all)
apply (rule ext, clarsimp, fast intro: exp_agrees)
done

lemma aborts_agrees[rule_format]:
  aborts C σ ⟹ ∀s'. agrees (fvC C) (fst σ) s' ⟶ snd σ = h' ⟶ aborts C (s', h')
by (erule aborts.induct, simp_all, auto simp add: writes_agrees accesses_agrees exp_agrees,
    auto simp add: agrees_def)

Corollaries of Proposition 4.2, useful for automation.

corollary exp_agrees2[simp]:

x ∉ fvE E

edenot E (s(x := v)) = edenot E s

by (rule exp_agrees, simp add: agrees_def)

corollary bexp_agrees2[simp]:

x ∉ fvB B

bdenot B (s(x := v)) = bdenot B s

by (rule bexp_agrees, simp add: agrees_def)

end