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

SharedMemory: independent_threads

Browse source
This commit is contained in:
Adam Chlipala 2016-04-22 18:25:07 -04:00
parent ec5a4a198e
commit 784c89332d
2 changed files with 58 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
Frap.v
View file

@ -59,9 +59,15 @@ Ltac fancy_neq :=
repeat match goal with
| _ => maps_neq
| [ H : @eq (nat -> _) _ _ |- _ ] => apply (f_equal (fun f => f 0)) in H
| [ H : _ = _ |- _ ] => invert H
| [ H : @eq ?T _ _ |- _ ] =>
match eval compute in T with
| fmap _ _ => fail 1
| _ => invert H
end
end.
Ltac maps_equal' := progress Frap.Map.M.maps_equal; autorewrite with core; simpl.
Ltac removeDups :=
match goal with
| [ |- context[constant ?ls] ] =>
@ -69,7 +75,16 @@ Ltac removeDups :=
erewrite (@removeDups_ok _ ls)
by repeat (apply RdNil
|| (apply RdNew; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ])
|| (apply RdDup; [ simpl; intuition congruence | ]))
|| (apply RdDup; [ simpl; intuition (congruence || (repeat (maps_equal' || f_equal))) | ]))
end.
Ltac doSubtract :=
match goal with
| [ |- context[constant ?ls \setminus constant ?ls0] ] =>
erewrite (@doSubtract_ok _ ls ls0)
by repeat (apply DsNil
|| (apply DsKeep; [ simpl; intuition (congruence || solve [ fancy_neq ]) | ])
|| (apply DsDrop; [ simpl; intuition (congruence || (repeat (maps_equal' || f_equal))) | ]))
end.
Ltac simpl_maps :=

44
SharedMemory.v
View file

@ -111,7 +111,8 @@ Theorem two_increments_ok :
(fun p => let '(_, _, c) := p in
notAboutToFail c = true).
Proof.
unfold two_increments, two_increments_thread.
Admitted.
(* unfold two_increments, two_increments_thread.
simplify.
eapply invariant_weaken.
apply multiStepClosure_ok; simplify.
@ -138,7 +139,7 @@ Proof.
simplify.
propositional; subst; equality.
Qed.
Qed.*)
(** * Optimization #1: always run all purely local actions first. *)
@ -476,7 +477,8 @@ Theorem two_increments_ok_again :
(fun p => let '(_, _, c) := p in
notAboutToFail c = true).
Proof.
apply step_stepL.
Admitted.
(* apply step_stepL.
unfold two_increments, two_increments_thread.
simplify.
eapply invariant_weaken.
@ -493,6 +495,42 @@ Proof.
model_check_step.
model_check_done.
simplify.
propositional; subst; equality.
Qed.*)
(** * Optimization #2: partial-order reduction *)
Example independent_threads :=
_ <- ((a <- Read 0;
Write 1 (a + 1))
|| (b <- Read 2;
Write 2 (b + 1)));
a <- Read 1;
if a ==n 1 then
Return 0
else
Fail.
Theorem independent_threads_ok :
invariantFor (trsys_of $0 {} independent_threads)
(fun p => let '(_, _, c) := p in
notAboutToFail c = true).
Proof.
apply step_stepL.
unfold independent_threads.
simplify.
eapply invariant_weaken.
apply multiStepClosure_ok; simplify.
model_check_step.
model_check_step.
model_check_step.
model_check_step.
model_check_step.
model_check_done.
simplify.
propositional; subst; equality.
Qed.