pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

TransitionSystems: give more meaningful names to parallel trsys components

Browse source
This commit is contained in:
Ben Sherman 2018-02-21 16:45:15 -05:00
parent 49b23293ca
commit 1d105aef0e
2 changed files with 16 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
TransitionSystems.v
View file

@ -368,16 +368,16 @@ Definition increment_sys := {|
* system the type of shared state remains the same, we take the Cartesian * system the type of shared state remains the same, we take the Cartesian
* product of the sets of private state. *) * product of the sets of private state. *)
Inductive parallel1 shared private1 private2 Inductive parallel_init shared private1 private2
(init1 : threaded_state shared private1 -> Prop) (init1 : threaded_state shared private1 -> Prop)
(init2 : threaded_state shared private2 -> Prop) (init2 : threaded_state shared private2 -> Prop)
: threaded_state shared (private1 * private2) -> Prop := : threaded_state shared (private1 * private2) -> Prop :=
| Pinit : forall sh pr1 pr2, | Pinit : forall sh pr1 pr2,
init1 {| Shared := sh; Private := pr1 |} init1 {| Shared := sh; Private := pr1 |}
-> init2 {| Shared := sh; Private := pr2 |} -> init2 {| Shared := sh; Private := pr2 |}
-> parallel1 init1 init2 {| Shared := sh; Private := (pr1, pr2) |}. -> parallel_init init1 init2 {| Shared := sh; Private := (pr1, pr2) |}.
Inductive parallel2 shared private1 private2 Inductive parallel_step shared private1 private2
(step1 : threaded_state shared private1 -> threaded_state shared private1 -> Prop) (step1 : threaded_state shared private1 -> threaded_state shared private1 -> Prop)
(step2 : threaded_state shared private2 -> threaded_state shared private2 -> Prop) (step2 : threaded_state shared private2 -> threaded_state shared private2 -> Prop)
: threaded_state shared (private1 * private2) : threaded_state shared (private1 * private2)
@ -385,19 +385,19 @@ Inductive parallel2 shared private1 private2
| Pstep1 : forall sh pr1 pr2 sh' pr1', | Pstep1 : forall sh pr1 pr2 sh' pr1',
(* First thread gets to run. *) (* First thread gets to run. *)
step1 {| Shared := sh; Private := pr1 |} {| Shared := sh'; Private := pr1' |} step1 {| Shared := sh; Private := pr1 |} {| Shared := sh'; Private := pr1' |}
-> parallel2 step1 step2 {| Shared := sh; Private := (pr1, pr2) |} -> parallel_step step1 step2 {| Shared := sh; Private := (pr1, pr2) |}
{| Shared := sh'; Private := (pr1', pr2) |} {| Shared := sh'; Private := (pr1', pr2) |}
| Pstep2 : forall sh pr1 pr2 sh' pr2', | Pstep2 : forall sh pr1 pr2 sh' pr2',
(* Second thread gets to run. *) (* Second thread gets to run. *)
step2 {| Shared := sh; Private := pr2 |} {| Shared := sh'; Private := pr2' |} step2 {| Shared := sh; Private := pr2 |} {| Shared := sh'; Private := pr2' |}
-> parallel2 step1 step2 {| Shared := sh; Private := (pr1, pr2) |} -> parallel_step step1 step2 {| Shared := sh; Private := (pr1, pr2) |}
{| Shared := sh'; Private := (pr1, pr2') |}. {| Shared := sh'; Private := (pr1, pr2') |}.
Definition parallel shared private1 private2 Definition parallel shared private1 private2
(sys1 : trsys (threaded_state shared private1)) (sys1 : trsys (threaded_state shared private1))
(sys2 : trsys (threaded_state shared private2)) := {| (sys2 : trsys (threaded_state shared private2)) := {|
Initial := parallel1 sys1.(Initial) sys2.(Initial); Initial := parallel_init sys1.(Initial) sys2.(Initial);
Step := parallel2 sys1.(Step) sys2.(Step) Step := parallel_step sys1.(Step) sys2.(Step)
|}. |}.
(* Example: composing two threads of the kind we formalized earlier *) (* Example: composing two threads of the kind we formalized earlier *)
@ -630,9 +630,9 @@ Proof.
apply invariant_induction; simplify; apply invariant_induction; simplify;
repeat match goal with repeat match goal with
| [ H : increment2_invariant _ |- _ ] => invert H | [ H : increment2_invariant _ |- _ ] => invert H
| [ H : parallel1 _ _ _ |- _ ] => invert H | [ H : parallel_init _ _ _ |- _ ] => invert H
| [ H : increment_init _ |- _ ] => invert H | [ H : increment_init _ |- _ ] => invert H
| [ H : parallel2 _ _ _ _ |- _ ] => invert H | [ H : parallel_step _ _ _ _ |- _ ] => invert H
| [ H : increment_step _ _ |- _ ] => invert H | [ H : increment_step _ _ |- _ ] => invert H
| [ pr : increment_program |- _ ] => cases pr; simplify | [ pr : increment_program |- _ ] => cases pr; simplify
end; try equality; end; try equality;

14
TransitionSystems_template.v
View file

@ -270,16 +270,16 @@ Definition increment_sys := {|
* system the type of shared state remains the same, we take the Cartesian * system the type of shared state remains the same, we take the Cartesian
* product of the sets of private state. *) * product of the sets of private state. *)
Inductive parallel1 shared private1 private2 Inductive parallel_init shared private1 private2
(init1 : threaded_state shared private1 -> Prop) (init1 : threaded_state shared private1 -> Prop)
(init2 : threaded_state shared private2 -> Prop) (init2 : threaded_state shared private2 -> Prop)
: threaded_state shared (private1 * private2) -> Prop := : threaded_state shared (private1 * private2) -> Prop :=
| Pinit : forall sh pr1 pr2, | Pinit : forall sh pr1 pr2,
init1 {| Shared := sh; Private := pr1 |} init1 {| Shared := sh; Private := pr1 |}
-> init2 {| Shared := sh; Private := pr2 |} -> init2 {| Shared := sh; Private := pr2 |}
-> parallel1 init1 init2 {| Shared := sh; Private := (pr1, pr2) |}. -> parallel_init init1 init2 {| Shared := sh; Private := (pr1, pr2) |}.
Inductive parallel2 shared private1 private2 Inductive parallel_step shared private1 private2
(step1 : threaded_state shared private1 -> threaded_state shared private1 -> Prop) (step1 : threaded_state shared private1 -> threaded_state shared private1 -> Prop)
(step2 : threaded_state shared private2 -> threaded_state shared private2 -> Prop) (step2 : threaded_state shared private2 -> threaded_state shared private2 -> Prop)
: threaded_state shared (private1 * private2) : threaded_state shared (private1 * private2)
@ -287,19 +287,19 @@ Inductive parallel2 shared private1 private2
| Pstep1 : forall sh pr1 pr2 sh' pr1', | Pstep1 : forall sh pr1 pr2 sh' pr1',
(* First thread gets to run. *) (* First thread gets to run. *)
step1 {| Shared := sh; Private := pr1 |} {| Shared := sh'; Private := pr1' |} step1 {| Shared := sh; Private := pr1 |} {| Shared := sh'; Private := pr1' |}
-> parallel2 step1 step2 {| Shared := sh; Private := (pr1, pr2) |} -> parallel_step step1 step2 {| Shared := sh; Private := (pr1, pr2) |}
{| Shared := sh'; Private := (pr1', pr2) |} {| Shared := sh'; Private := (pr1', pr2) |}
| Pstep2 : forall sh pr1 pr2 sh' pr2', | Pstep2 : forall sh pr1 pr2 sh' pr2',
(* Second thread gets to run. *) (* Second thread gets to run. *)
step2 {| Shared := sh; Private := pr2 |} {| Shared := sh'; Private := pr2' |} step2 {| Shared := sh; Private := pr2 |} {| Shared := sh'; Private := pr2' |}
-> parallel2 step1 step2 {| Shared := sh; Private := (pr1, pr2) |} -> parallel_step step1 step2 {| Shared := sh; Private := (pr1, pr2) |}
{| Shared := sh'; Private := (pr1, pr2') |}. {| Shared := sh'; Private := (pr1, pr2') |}.
Definition parallel shared private1 private2 Definition parallel shared private1 private2
(sys1 : trsys (threaded_state shared private1)) (sys1 : trsys (threaded_state shared private1))
(sys2 : trsys (threaded_state shared private2)) := {| (sys2 : trsys (threaded_state shared private2)) := {|
Initial := parallel1 sys1.(Initial) sys2.(Initial); Initial := parallel_init sys1.(Initial) sys2.(Initial);
Step := parallel2 sys1.(Step) sys2.(Step) Step := parallel_step sys1.(Step) sys2.(Step)
|}. |}.
(* Example: composing two threads of the kind we formalized earlier *) (* Example: composing two threads of the kind we formalized earlier *)