mirror of
https://github.com/achlipala/frap.git
synced 2024-11-10 00:07:51 +00:00
OperationalSemantics_template (really this time)
This commit is contained in:
Adam Chlipala
parent
c4d622f7a1
commit
96327eb9aa
1 changed files with 903 additions and 0 deletions
903
OperationalSemantics_template.v
Normal file
903
OperationalSemantics_template.v
Normal file
|
|
@ -0,0 +1,903 @@
|
|||
(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
|
||||
* Chapter 6: Operational Semantics
|
||||
* Author: Adam Chlipala
|
||||
* License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
|
||||
|
||||
Require Import Frap.
|
||||
|
||||
Set Implicit Arguments.
|
||||
|
||||
|
||||
(* OK, enough with defining transition relations manually. Let's return to our
|
||||
* syntax of imperative programs from Chapter 3. *)
|
||||
|
||||
Inductive arith : Set :=
|
||||
| Const (n : nat)
|
||||
| Var (x : var)
|
||||
| Plus (e1 e2 : arith)
|
||||
| Minus (e1 e2 : arith)
|
||||
| Times (e1 e2 : arith).
|
||||
|
||||
Inductive cmd :=
|
||||
| Skip
|
||||
| Assign (x : var) (e : arith)
|
||||
| Sequence (c1 c2 : cmd)
|
||||
| If (e : arith) (then_ else_ : cmd)
|
||||
| While (e : arith) (body : cmd).
|
||||
(* Important differences: we added [If] and switched [Repeat] to general
|
||||
* [While]. *)
|
||||
|
||||
(* Here are some notations for the language, which again we won't really
|
||||
* explain. *)
|
||||
Coercion Const : nat >-> arith.
|
||||
Coercion Var : var >-> arith.
|
||||
Infix "+" := Plus : arith_scope.
|
||||
Infix "-" := Minus : arith_scope.
|
||||
Infix "*" := Times : arith_scope.
|
||||
Delimit Scope arith_scope with arith.
|
||||
Notation "x <- e" := (Assign x e%arith) (at level 75).
|
||||
Infix ";;" := Sequence (at level 76). (* This one changed slightly, to avoid parsing clashes. *)
|
||||
Notation "'when' e 'then' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0).
|
||||
Notation "'while' e 'loop' body 'done'" := (While e%arith body) (at level 75).
|
||||
|
||||
(* Here's an adaptation of our factorial example from Chapter 3. *)
|
||||
Example factorial :=
|
||||
"output" <- 1;;
|
||||
while "input" loop
|
||||
"output" <- "output" * "input";;
|
||||
"input" <- "input" - 1
|
||||
done.
|
||||
|
||||
(* Recall our use of a recursive function to interpret expressions. *)
|
||||
Definition valuation := fmap var nat.
|
||||
Fixpoint interp (e : arith) (v : valuation) : nat :=
|
||||
match e with
|
||||
| Const n => n
|
||||
| Var x =>
|
||||
match v $? x with
|
||||
| None => 0
|
||||
| Some n => n
|
||||
end
|
||||
| Plus e1 e2 => interp e1 v + interp e2 v
|
||||
| Minus e1 e2 => interp e1 v - interp e2 v
|
||||
| Times e1 e2 => interp e1 v * interp e2 v
|
||||
end.
|
||||
|
||||
(* Our old trick of interpreters won't work for this new language, because of
|
||||
* the general "while" loops. No such interpreter could terminate for all
|
||||
* programs. Instead, we will use inductive predicates to explain program
|
||||
* meanings. First, let's apply the most intuitive method, called
|
||||
* *big-step operational semantics*. *)
|
||||
Inductive eval : valuation -> cmd -> valuation -> Prop :=
|
||||
| EvalSkip : forall v,
|
||||
eval v Skip v
|
||||
| EvalAssign : forall v x e,
|
||||
eval v (Assign x e) (v $+ (x, interp e v))
|
||||
| EvalSeq : forall v c1 v1 c2 v2,
|
||||
eval v c1 v1
|
||||
-> eval v1 c2 v2
|
||||
-> eval v (Sequence c1 c2) v2
|
||||
| EvalIfTrue : forall v e then_ else_ v',
|
||||
interp e v <> 0
|
||||
-> eval v then_ v'
|
||||
-> eval v (If e then_ else_) v'
|
||||
| EvalIfFalse : forall v e then_ else_ v',
|
||||
interp e v = 0
|
||||
-> eval v else_ v'
|
||||
-> eval v (If e then_ else_) v'
|
||||
| EvalWhileTrue : forall v e body v' v'',
|
||||
interp e v <> 0
|
||||
-> eval v body v'
|
||||
-> eval v' (While e body) v''
|
||||
-> eval v (While e body) v''
|
||||
| EvalWhileFalse : forall v e body,
|
||||
interp e v = 0
|
||||
-> eval v (While e body) v.
|
||||
|
||||
(* Let's run the factorial program on a few inputs. *)
|
||||
Theorem factorial_2 : exists v, eval ($0 $+ ("input", 2)) factorial v
|
||||
/\ v $? "output" = Some 2.
|
||||
Proof.
|
||||
eexists; propositional.
|
||||
(* [eexists]: to prove [exists x, P(x)], switch to proving [P(?y)], for a new
|
||||
* existential variable [?y]. *)
|
||||
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
simplify.
|
||||
equality.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
simplify.
|
||||
equality.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
apply EvalWhileFalse.
|
||||
(* Note that, for this step, we had to specify which rule to use, since
|
||||
* otherwise [econstructor] incorrectly guesses [EvalWhileTrue]. *)
|
||||
simplify.
|
||||
equality.
|
||||
|
||||
simplify.
|
||||
equality.
|
||||
Qed.
|
||||
|
||||
(* That was rather repetitive. It's easy to automate. *)
|
||||
|
||||
Ltac eval1 :=
|
||||
apply EvalSkip || apply EvalAssign || eapply EvalSeq
|
||||
|| (apply EvalIfTrue; [ simplify; equality | ])
|
||||
|| (apply EvalIfFalse; [ simplify; equality | ])
|
||||
|| (eapply EvalWhileTrue; [ simplify; equality | | ])
|
||||
|| (apply EvalWhileFalse; [ simplify; equality ]).
|
||||
Ltac evaluate := simplify; try equality; repeat eval1.
|
||||
|
||||
Theorem factorial_2_snazzy : exists v, eval ($0 $+ ("input", 2)) factorial v
|
||||
/\ v $? "output" = Some 2.
|
||||
Proof.
|
||||
eexists; propositional.
|
||||
evaluate.
|
||||
evaluate.
|
||||
Qed.
|
||||
|
||||
Theorem factorial_3 : exists v, eval ($0 $+ ("input", 3)) factorial v
|
||||
/\ v $? "output" = Some 6.
|
||||
Proof.
|
||||
eexists; propositional.
|
||||
evaluate.
|
||||
evaluate.
|
||||
Qed.
|
||||
|
||||
(* Instead of chugging through these relatively slow individual executions,
|
||||
* let's prove once and for all that [factorial] is correct. *)
|
||||
Fixpoint fact (n : nat) : nat :=
|
||||
match n with
|
||||
| O => 1
|
||||
| S n' => n * fact n'
|
||||
end.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Example factorial_loop :=
|
||||
while "input" loop
|
||||
"output" <- "output" * "input";;
|
||||
"input" <- "input" - 1
|
||||
done.
|
||||
|
||||
Lemma factorial_loop_correct : forall n v out, v $? "input" = Some n
|
||||
-> v $? "output" = Some out
|
||||
-> exists v', eval v factorial_loop v'
|
||||
/\ v' $? "output" = Some (fact n * out).
|
||||
Proof.
|
||||
induct n; simplify.
|
||||
|
||||
exists v; propositional.
|
||||
apply EvalWhileFalse.
|
||||
simplify.
|
||||
rewrite H.
|
||||
equality.
|
||||
rewrite H0.
|
||||
f_equal.
|
||||
ring.
|
||||
|
||||
assert (exists v', eval (v $+ ("output", out * S n) $+ ("input", n)) factorial_loop v'
|
||||
/\ v' $? "output" = Some (fact n * (out * S n))).
|
||||
apply IHn.
|
||||
simplify; equality.
|
||||
simplify; equality.
|
||||
first_order.
|
||||
eexists; propositional.
|
||||
econstructor.
|
||||
simplify.
|
||||
rewrite H.
|
||||
equality.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
simplify.
|
||||
rewrite H, H0.
|
||||
replace (S n - 1) with n by linear_arithmetic.
|
||||
(* [replace e1 with e2 by tac]: replace occurrences of [e1] with [e2], proving
|
||||
* [e2 = e1] with tactic [tac]. *)
|
||||
apply H1.
|
||||
rewrite H2.
|
||||
f_equal.
|
||||
ring.
|
||||
Qed.
|
||||
|
||||
Theorem factorial_correct : forall n v, v $? "input" = Some n
|
||||
-> exists v', eval v factorial v'
|
||||
/\ v' $? "output" = Some (fact n).
|
||||
Proof.
|
||||
simplify.
|
||||
assert (exists v', eval (v $+ ("output", 1)) factorial_loop v'
|
||||
/\ v' $? "output" = Some (fact n * 1)).
|
||||
apply factorial_loop_correct.
|
||||
simplify; equality.
|
||||
simplify; equality.
|
||||
first_order.
|
||||
eexists; propositional.
|
||||
econstructor.
|
||||
econstructor.
|
||||
simplify.
|
||||
apply H0.
|
||||
rewrite H1.
|
||||
f_equal.
|
||||
ring.
|
||||
Qed.
|
||||
|
||||
|
||||
(** * Small-step semantics *)
|
||||
|
||||
(* Big-step semantics only tells us something about the behavior of terminating
|
||||
* programs. Our imperative language clearly supports nontermination, thanks to
|
||||
* the inclusion of general "while" loops. A switch to *small-step* semantics
|
||||
* lets us also explain what happens with nonterminating executions, and this
|
||||
* style will also come in handy for more advanced features like concurrency. *)
|
||||
|
||||
Inductive step : valuation * cmd -> valuation * cmd -> Prop :=
|
||||
| StepAssign : forall v x e,
|
||||
step (v, Assign x e) (v $+ (x, interp e v), Skip)
|
||||
| StepSeq1 : forall v c1 c2 v' c1',
|
||||
step (v, c1) (v', c1')
|
||||
-> step (v, Sequence c1 c2) (v', Sequence c1' c2)
|
||||
| StepSeq2 : forall v c2,
|
||||
step (v, Sequence Skip c2) (v, c2)
|
||||
| StepIfTrue : forall v e then_ else_,
|
||||
interp e v <> 0
|
||||
-> step (v, If e then_ else_) (v, then_)
|
||||
| StepIfFalse : forall v e then_ else_,
|
||||
interp e v = 0
|
||||
-> step (v, If e then_ else_) (v, else_)
|
||||
| StepWhileTrue : forall v e body,
|
||||
interp e v <> 0
|
||||
-> step (v, While e body) (v, Sequence body (While e body))
|
||||
| StepWhileFalse : forall v e body,
|
||||
interp e v = 0
|
||||
-> step (v, While e body) (v, Skip).
|
||||
|
||||
(* Here's a small-step factorial execution. *)
|
||||
Theorem factorial_2_small : exists v, step^* ($0 $+ ("input", 2), factorial) (v, Skip)
|
||||
/\ v $? "output" = Some 2.
|
||||
Proof.
|
||||
eexists; propositional.
|
||||
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
apply StepSeq2.
|
||||
econstructor.
|
||||
econstructor.
|
||||
simplify.
|
||||
equality.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
apply StepSeq2.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
apply StepSeq2.
|
||||
econstructor.
|
||||
econstructor.
|
||||
simplify.
|
||||
equality.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
apply StepSeq2.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
econstructor.
|
||||
apply StepSeq2.
|
||||
econstructor.
|
||||
apply StepWhileFalse.
|
||||
simplify.
|
||||
equality.
|
||||
econstructor.
|
||||
|
||||
simplify.
|
||||
equality.
|
||||
Qed.
|
||||
|
||||
Ltac step1 :=
|
||||
apply TrcRefl || eapply TrcFront
|
||||
|| apply StepAssign || apply StepSeq2 || eapply StepSeq1
|
||||
|| (apply StepIfTrue; [ simplify; equality ])
|
||||
|| (apply StepIfFalse; [ simplify; equality ])
|
||||
|| (eapply StepWhileTrue; [ simplify; equality ])
|
||||
|| (apply StepWhileFalse; [ simplify; equality ]).
|
||||
Ltac stepper := simplify; try equality; repeat step1.
|
||||
|
||||
Theorem factorial_2_small_snazzy : exists v, step^* ($0 $+ ("input", 2), factorial) (v, Skip)
|
||||
/\ v $? "output" = Some 2.
|
||||
Proof.
|
||||
eexists; propositional.
|
||||
|
||||
stepper.
|
||||
stepper.
|
||||
Qed.
|
||||
|
||||
(* It turns out that these two semantics styles are equivalent. Let's prove
|
||||
* it. *)
|
||||
|
||||
(* Automated proofs used here, if only to save time in class.
|
||||
* See book code for more manual proofs, too. *)
|
||||
|
||||
Hint Constructors trc step eval.
|
||||
|
||||
Theorem big_small : forall v c v', eval v c v'
|
||||
-> step^* (v, c) (v', Skip).
|
||||
Proof.
|
||||
Admitted.
|
||||
|
||||
Theorem small_big_snazzy : forall v c v', step^* (v, c) (v', Skip)
|
||||
-> eval v c v'.
|
||||
Proof.
|
||||
Admitted.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(** * Small-step semantics gives rise to transition systems. *)
|
||||
|
||||
Definition trsys_of (v : valuation) (c : cmd) : trsys (valuation * cmd) := {|
|
||||
Initial := {(v, c)};
|
||||
Step := step
|
||||
|}.
|
||||
|
||||
Theorem simple_invariant :
|
||||
invariantFor (trsys_of ($0 $+ ("a", 1)) ("b" <- "a" + 1;; "c" <- "b" + "b"))
|
||||
(fun s => snd s = Skip -> fst s $? "c" = Some 4).
|
||||
Proof.
|
||||
model_check.
|
||||
Qed.
|
||||
|
||||
Inductive isEven : nat -> Prop :=
|
||||
| EvenO : isEven 0
|
||||
| EvenSS : forall n, isEven n -> isEven (S (S n)).
|
||||
|
||||
Lemma isEven_minus2 : forall n, isEven n -> isEven (n - 2).
|
||||
Proof.
|
||||
induct 1; simplify.
|
||||
|
||||
constructor.
|
||||
|
||||
replace (n - 0) with n by linear_arithmetic.
|
||||
assumption.
|
||||
Qed.
|
||||
|
||||
Lemma isEven_plus : forall n m,
|
||||
isEven n
|
||||
-> isEven m
|
||||
-> isEven (n + m).
|
||||
Proof.
|
||||
induct 1; simplify.
|
||||
|
||||
assumption.
|
||||
|
||||
constructor.
|
||||
apply IHisEven.
|
||||
assumption.
|
||||
Qed.
|
||||
|
||||
Hint Constructors isEven.
|
||||
Hint Resolve isEven_minus2 isEven_plus.
|
||||
|
||||
Definition my_loop :=
|
||||
while "n" loop
|
||||
"a" <- "a" + "n";;
|
||||
"n" <- "n" - 2
|
||||
done.
|
||||
|
||||
Theorem manually_proved_invariant : forall n,
|
||||
isEven n
|
||||
-> invariantFor (trsys_of ($0 $+ ("n", n) $+ ("a", 0)) (while "n" loop "a" <- "a" + "n";; "n" <- "n" - 2 done))
|
||||
(fun s => exists a, fst s $? "a" = Some a /\ isEven a).
|
||||
Proof.
|
||||
Admitted.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Definition all_programs := {
|
||||
(while "n" loop
|
||||
"a" <- "a" + "n";;
|
||||
"n" <- "n" - 2
|
||||
done),
|
||||
("a" <- "a" + "n";;
|
||||
"n" <- "n" - 2),
|
||||
(Skip;;
|
||||
"n" <- "n" - 2),
|
||||
("n" <- "n" - 2),
|
||||
(("a" <- "a" + "n";;
|
||||
"n" <- "n" - 2);;
|
||||
while "n" loop
|
||||
"a" <- "a" + "n";;
|
||||
"n" <- "n" - 2
|
||||
done),
|
||||
((Skip;;
|
||||
"n" <- "n" - 2);;
|
||||
while "n" loop
|
||||
"a" <- "a" + "n";;
|
||||
"n" <- "n" - 2
|
||||
done),
|
||||
("n" <- "n" - 2;;
|
||||
while "n" loop
|
||||
"a" <- "a" + "n";;
|
||||
"n" <- "n" - 2
|
||||
done),
|
||||
(Skip;;
|
||||
while "n" loop
|
||||
"a" <- "a" + "n";;
|
||||
"n" <- "n" - 2
|
||||
done),
|
||||
Skip
|
||||
}.
|
||||
|
||||
Lemma manually_proved_invariant' : forall n,
|
||||
isEven n
|
||||
-> invariantFor (trsys_of ($0 $+ ("n", n) $+ ("a", 0)) (while "n" loop "a" <- "a" + "n";; "n" <- "n" - 2 done))
|
||||
(fun s => all_programs (snd s)
|
||||
/\ exists n a, fst s $? "n" = Some n
|
||||
/\ fst s $? "a" = Some a
|
||||
/\ isEven n
|
||||
/\ isEven a).
|
||||
Proof.
|
||||
simplify; apply invariant_induction; simplify; unfold all_programs in *; first_order; subst; simplify;
|
||||
try match goal with
|
||||
| [ H : step _ _ |- _ ] => invert H; simplify
|
||||
end;
|
||||
repeat (match goal with
|
||||
| [ H : _ = Some _ |- _ ] => rewrite H
|
||||
| [ H : @eq cmd (_ _ _) _ |- _ ] => invert H
|
||||
| [ H : @eq cmd (_ _ _ _) _ |- _ ] => invert H
|
||||
| [ H : step _ _ |- _ ] => invert2 H
|
||||
end; simplify); equality || eauto 7.
|
||||
Qed.
|
||||
|
||||
(* We'll return to these systems and their abstractions in the next few
|
||||
* chapters. *)
|
||||
|
||||
|
||||
(** * Contextual small-step semantics *)
|
||||
|
||||
(* There is a common way to factor a small-step semantics into different parts,
|
||||
* to make the semantics easier to understand and extend. First, we define a
|
||||
* notion of *evaluation contexts*, which are commands with *holes* in them. *)
|
||||
Inductive context :=
|
||||
| Hole
|
||||
| CSeq (C : context) (c : cmd).
|
||||
|
||||
(* This relation explains how to plug the hole in a context with a specific
|
||||
* term. Note that we use an inductive relation instead of a recursive
|
||||
* definition, because Coq's proof automation is better at working with
|
||||
* relations. *)
|
||||
Inductive plug : context -> cmd -> cmd -> Prop :=
|
||||
| PlugHole : forall c, plug Hole c c
|
||||
| PlugSeq : forall c C c' c2,
|
||||
plug C c c'
|
||||
-> plug (CSeq C c2) c (Sequence c' c2).
|
||||
|
||||
(* Now we define almost the same step relation as before, with one omission:
|
||||
* only the more trivial of the [Sequence] rules remains. *)
|
||||
Inductive step0 : valuation * cmd -> valuation * cmd -> Prop :=
|
||||
| Step0Assign : forall v x e,
|
||||
step0 (v, Assign x e) (v $+ (x, interp e v), Skip)
|
||||
| Step0Seq : forall v c2,
|
||||
step0 (v, Sequence Skip c2) (v, c2)
|
||||
| Step0IfTrue : forall v e then_ else_,
|
||||
interp e v <> 0
|
||||
-> step0 (v, If e then_ else_) (v, then_)
|
||||
| Step0IfFalse : forall v e then_ else_,
|
||||
interp e v = 0
|
||||
-> step0 (v, If e then_ else_) (v, else_)
|
||||
| Step0WhileTrue : forall v e body,
|
||||
interp e v <> 0
|
||||
-> step0 (v, While e body) (v, Sequence body (While e body))
|
||||
| Step0WhileFalse : forall v e body,
|
||||
interp e v = 0
|
||||
-> step0 (v, While e body) (v, Skip).
|
||||
|
||||
(* We recover the meaning of the original with one top-level rule, combining
|
||||
* plugging of contexts with basic steps. *)
|
||||
Inductive cstep : valuation * cmd -> valuation * cmd -> Prop :=
|
||||
| CStep : forall C v c v' c' c1 c2,
|
||||
plug C c c1
|
||||
-> step0 (v, c) (v', c')
|
||||
-> plug C c' c2
|
||||
-> cstep (v, c1) (v', c2).
|
||||
|
||||
(* We can prove equivalence between the two formulations. *)
|
||||
|
||||
Hint Constructors plug step0 cstep.
|
||||
|
||||
Theorem step_cstep : forall v c v' c',
|
||||
step (v, c) (v', c')
|
||||
-> cstep (v, c) (v', c').
|
||||
Proof.
|
||||
Admitted.
|
||||
|
||||
Theorem cstep_step : forall v c v' c',
|
||||
cstep (v, c) (v', c')
|
||||
-> step (v, c) (v', c').
|
||||
Proof.
|
||||
Admitted.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(** * Example of how easy it is to add concurrency to a contextual semantics *)
|
||||
|
||||
Module Concurrent.
|
||||
(* Let's add a construct for *parallel execution* of two commands. Such
|
||||
* parallelism may be nested arbitrarily. *)
|
||||
Inductive cmd :=
|
||||
| Skip
|
||||
| Assign (x : var) (e : arith)
|
||||
| Sequence (c1 c2 : cmd)
|
||||
| If (e : arith) (then_ else_ : cmd)
|
||||
| While (e : arith) (body : cmd)
|
||||
| Parallel (c1 c2 : cmd).
|
||||
|
||||
Notation "x <- e" := (Assign x e%arith) (at level 75).
|
||||
Infix ";;" := Sequence (at level 76). (* This one changed slightly, to avoid parsing clashes. *)
|
||||
Notation "'when' e 'then' then_ 'else' else_ 'done'" := (If e%arith then_ else_) (at level 75, e at level 0).
|
||||
Notation "'while' e 'loop' body 'done'" := (While e%arith body) (at level 75).
|
||||
Infix "||" := Parallel.
|
||||
|
||||
|
||||
(* We need surprisingly few changes to the contextual semantics, to explain
|
||||
* this new feature. First, we allow a hole to appear on *either side* of a
|
||||
* [Parallel]. In other words, the "scheduler" may choose either "thread" to
|
||||
* run next. *)
|
||||
Inductive context :=
|
||||
| Hole
|
||||
| CSeq (C : context) (c : cmd)
|
||||
| CPar1 (C : context) (c : cmd)
|
||||
| CPar2 (c : cmd) (C : context).
|
||||
|
||||
(* We explain the meaning of plugging the new contexts in the obvious way. *)
|
||||
Inductive plug : context -> cmd -> cmd -> Prop :=
|
||||
| PlugHole : forall c, plug Hole c c
|
||||
| PlugSeq : forall c C c' c2,
|
||||
plug C c c'
|
||||
-> plug (CSeq C c2) c (Sequence c' c2)
|
||||
| PlugPar1 : forall c C c' c2,
|
||||
plug C c c'
|
||||
-> plug (CPar1 C c2) c (Parallel c' c2)
|
||||
| PlugPar2 : forall c C c' c1,
|
||||
plug C c c'
|
||||
-> plug (CPar2 c1 C) c (Parallel c1 c').
|
||||
|
||||
(* The only new step rules are for "cleaning up" finished "threads," which
|
||||
* have reached the point of being [Skip] commands. *)
|
||||
Inductive step0 : valuation * cmd -> valuation * cmd -> Prop :=
|
||||
| Step0Assign : forall v x e,
|
||||
step0 (v, Assign x e) (v $+ (x, interp e v), Skip)
|
||||
| Step0Seq : forall v c2,
|
||||
step0 (v, Sequence Skip c2) (v, c2)
|
||||
| Step0IfTrue : forall v e then_ else_,
|
||||
interp e v <> 0
|
||||
-> step0 (v, If e then_ else_) (v, then_)
|
||||
| Step0IfFalse : forall v e then_ else_,
|
||||
interp e v = 0
|
||||
-> step0 (v, If e then_ else_) (v, else_)
|
||||
| Step0WhileTrue : forall v e body,
|
||||
interp e v <> 0
|
||||
-> step0 (v, While e body) (v, Sequence body (While e body))
|
||||
| Step0WhileFalse : forall v e body,
|
||||
interp e v = 0
|
||||
-> step0 (v, While e body) (v, Skip)
|
||||
| Step0Par1 : forall v c,
|
||||
step0 (v, Parallel Skip c) (v, c).
|
||||
|
||||
Inductive cstep : valuation * cmd -> valuation * cmd -> Prop :=
|
||||
| CStep : forall C v c v' c' c1 c2,
|
||||
plug C c c1
|
||||
-> step0 (v, c) (v', c')
|
||||
-> plug C c' c2
|
||||
-> cstep (v, c1) (v', c2).
|
||||
|
||||
(** Example: stepping a specific program. *)
|
||||
|
||||
(* Here's the classic cautionary-tale program about remembering to lock your
|
||||
* concurrent threads. *)
|
||||
Definition prog :=
|
||||
("a" <- "n";;
|
||||
"n" <- "a" + 1)
|
||||
|| ("b" <- "n";;
|
||||
"n" <- "b" + 1).
|
||||
|
||||
Hint Constructors plug step0 cstep.
|
||||
|
||||
(* The naive "expected" answer is attainable. *)
|
||||
Theorem correctAnswer : forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip)
|
||||
/\ v $? "n" = Some (n + 2).
|
||||
Proof.
|
||||
eexists; propositional.
|
||||
unfold prog.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := CPar1 (CSeq Hole _) _); eauto.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := CPar1 Hole _); eauto.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := CPar1 Hole _); eauto.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := Hole); eauto.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := CSeq Hole _); eauto.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := Hole); eauto.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := Hole); eauto.
|
||||
|
||||
econstructor.
|
||||
|
||||
simplify.
|
||||
f_equal.
|
||||
ring.
|
||||
Qed.
|
||||
|
||||
(* But so is the "wrong" answer! *)
|
||||
Theorem wrongAnswer : forall n, exists v, cstep^* ($0 $+ ("n", n), prog) (v, Skip)
|
||||
/\ v $? "n" = Some (n + 1).
|
||||
Proof.
|
||||
eexists; propositional.
|
||||
unfold prog.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := CPar1 (CSeq Hole _) _); eauto.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := CPar2 _ (CSeq Hole _)); eauto.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := CPar1 Hole _); eauto.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := CPar2 _ Hole); eauto.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := CPar1 Hole _); eauto.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := Hole); eauto.
|
||||
|
||||
econstructor.
|
||||
eapply CStep with (C := Hole); eauto.
|
||||
|
||||
econstructor.
|
||||
|
||||
simplify.
|
||||
equality.
|
||||
Qed.
|
||||
|
||||
(** Proving equivalence with non-contextual semantics *)
|
||||
|
||||
(* To give us something interesting to prove, let's also define a
|
||||
* non-contextual small-step semantics. Note how we have to do some more
|
||||
* explicit threading of mutable state through recursive invocations. *)
|
||||
Inductive step : valuation * cmd -> valuation * cmd -> Prop :=
|
||||
| StepAssign : forall v x e,
|
||||
step (v, Assign x e) (v $+ (x, interp e v), Skip)
|
||||
| StepSeq1 : forall v c1 c2 v' c1',
|
||||
step (v, c1) (v', c1')
|
||||
-> step (v, Sequence c1 c2) (v', Sequence c1' c2)
|
||||
| StepSeq2 : forall v c2,
|
||||
step (v, Sequence Skip c2) (v, c2)
|
||||
| StepIfTrue : forall v e then_ else_,
|
||||
interp e v <> 0
|
||||
-> step (v, If e then_ else_) (v, then_)
|
||||
| StepIfFalse : forall v e then_ else_,
|
||||
interp e v = 0
|
||||
-> step (v, If e then_ else_) (v, else_)
|
||||
| StepWhileTrue : forall v e body,
|
||||
interp e v <> 0
|
||||
-> step (v, While e body) (v, Sequence body (While e body))
|
||||
| StepWhileFalse : forall v e body,
|
||||
interp e v = 0
|
||||
-> step (v, While e body) (v, Skip)
|
||||
| StepParSkip1 : forall v c,
|
||||
step (v, Parallel Skip c) (v, c)
|
||||
| StepPar1 : forall v c1 c2 v' c1',
|
||||
step (v, c1) (v', c1')
|
||||
-> step (v, Parallel c1 c2) (v', Parallel c1' c2)
|
||||
| StepPar2 : forall v c1 c2 v' c2',
|
||||
step (v, c2) (v', c2')
|
||||
-> step (v, Parallel c1 c2) (v', Parallel c1 c2').
|
||||
|
||||
Hint Constructors step.
|
||||
|
||||
(* Now, an automated proof of equivalence. Actually, it's *exactly* the same
|
||||
* proof we used for the old feature set! *)
|
||||
|
||||
Theorem step_cstep : forall v c v' c',
|
||||
step (v, c) (v', c')
|
||||
-> cstep (v, c) (v', c').
|
||||
Proof.
|
||||
induct 1; repeat match goal with
|
||||
| [ H : cstep _ _ |- _ ] => invert H
|
||||
end; eauto.
|
||||
Qed.
|
||||
|
||||
Hint Resolve step_cstep.
|
||||
|
||||
Lemma step0_step : forall v c v' c',
|
||||
step0 (v, c) (v', c')
|
||||
-> step (v, c) (v', c').
|
||||
Proof.
|
||||
induct 1; eauto.
|
||||
Qed.
|
||||
|
||||
Hint Resolve step0_step.
|
||||
|
||||
Lemma cstep_step' : forall C c0 c,
|
||||
plug C c0 c
|
||||
-> forall v' c'0 v c', step0 (v, c0) (v', c'0)
|
||||
-> plug C c'0 c'
|
||||
-> step (v, c) (v', c').
|
||||
Proof.
|
||||
induct 1; simplify; repeat match goal with
|
||||
| [ H : plug _ _ _ |- _ ] => invert1 H
|
||||
end; eauto.
|
||||
Qed.
|
||||
|
||||
Hint Resolve cstep_step'.
|
||||
|
||||
Theorem cstep_step : forall v c v' c',
|
||||
cstep (v, c) (v', c')
|
||||
-> step (v, c) (v', c').
|
||||
Proof.
|
||||
induct 1; eauto.
|
||||
Qed.
|
||||
End Concurrent.
|
||||
|
||||
|
||||
(** * Determinism *)
|
||||
|
||||
(* Each of the relations we have defined turns out to be deterministic. Let's
|
||||
* prove it. *)
|
||||
|
||||
Theorem eval_det : forall v c v1,
|
||||
eval v c v1
|
||||
-> forall v2, eval v c v2
|
||||
-> v1 = v2.
|
||||
Proof.
|
||||
induct 1; invert 1; try first_order.
|
||||
|
||||
apply IHeval2.
|
||||
apply IHeval1 in H5.
|
||||
subst.
|
||||
assumption.
|
||||
|
||||
apply IHeval2.
|
||||
apply IHeval1 in H7.
|
||||
subst.
|
||||
assumption.
|
||||
Qed.
|
||||
|
||||
Theorem step_det : forall s out1,
|
||||
step s out1
|
||||
-> forall out2, step s out2
|
||||
-> out1 = out2.
|
||||
Proof.
|
||||
induct 1; invert 1; try first_order.
|
||||
|
||||
apply IHstep in H5.
|
||||
equality.
|
||||
|
||||
invert H.
|
||||
|
||||
invert H4.
|
||||
Qed.
|
||||
|
||||
Theorem cstep_det : forall s out1,
|
||||
cstep s out1
|
||||
-> forall out2, cstep s out2
|
||||
-> out1 = out2.
|
||||
Proof.
|
||||
simplify.
|
||||
cases s; cases out1; cases out2.
|
||||
eapply step_det.
|
||||
apply cstep_step.
|
||||
eassumption.
|
||||
apply cstep_step.
|
||||
eassumption.
|
||||
Qed.
|
||||
Loading…
Reference in a new issue