Merge pull request #6 from harp-project/concurrency

Extend the formalisation of concurrency

erlang-playground/e.erl

@@ -1,5 +1,11 @@
 -module(e).
--compile(export_all).
+-export([f/0, obj_map/2]).
+
+obj_map(F, E) ->
+  case E of
+    [] -> [];
+    [H | T] -> [F(H) | obj_map(F, T)]
+  end.
 
 f() ->
   Pid = spawn(e, g, []),

erlang-playground/examples.core

@@ -0,0 +1,140 @@
+module 'examples' ['signal_ordering'/0,
+        'signal_ordering_2'/0,
+        'signal_ordering_3'/0,
+        'signal_ordering_4'/0,
+        'test_1'/0,
+        'test_2'/0,
+        'test_3'/0,
+        'test_4'/0,
+        'test_5'/0,
+        'test_6'/0,
+        'test_7'/0,
+        'test_8'/0,
+        'test_9'/0,
+		    'module_info'/0,
+		    'module_info'/1]
+    attributes [%% Line 1
+		'file' =
+		    %% Line 1
+		    [{[101|[120|[97|[109|[112|[108|[101|[115|[46|[101|[114|[108]]]]]]]]]]]],1}],
+		%% Line 2
+  	'compile' =
+		    %% Line 2
+		    ['export_all']]
+'module_info'/0 =
+    fun () ->
+	call 'erlang':'get_module_info'
+	    ('examples')
+'module_info'/1 =
+    fun (_0) ->
+	call 'erlang':'get_module_info'
+	    ('examples', _0)
+
+'signal_ordering'/0 = fun () ->
+  let F0 = fun() ->
+         receive {PID1, PID2} when 'true' -> 
+             let X = call 'erlang':'!'(PID1, 'fst') in
+               call 'erlang':'!'(PID2, 'snd')
+         after 'infinity' -> 'error'
+      in
+  let F1 = fun() ->
+         receive PID2 when call 'erlang':'is_pid'(PID2) ->
+                receive X when 'true' -> call 'erlang':'!'(PID2, X)
+                after 'infinity' -> 'error' 
+         after 'infinity' -> 'error'
+      in
+  let F2 = fun() ->
+           receive X when 'true' ->
+                receive Y when 'true' ->
+                    do do call 'io':'fwrite'('first message: ') call 'io':'fwrite'(X)
+                       do call 'io':'fwrite'('second message: ') call 'io':'fwrite'(Y)
+                after 'infinity' -> 'error'
+           after 'infinity' -> 'error'
+      in
+  let PID0 = call 'erlang':'spawn'(F0) in
+  let PID1 = call 'erlang':'spawn'(F1) in
+  let PID2 = call 'erlang':'spawn'(F2) in
+  let A = call 'erlang':'!'(PID0, {PID1, PID2}) in
+    do call 'erlang':'!'(PID1, PID2) 'ok'
+
+'signal_ordering_2'/0 = fun () ->
+  let F0 = fun() ->
+         receive {PID1, PID2} when 'true' -> 
+             let X = call 'erlang':'!'(PID1, 'fst') in
+               do call 'timer':'sleep'(1)
+                  call 'erlang':'!'(PID2, 'snd')
+         after 'infinity' -> 'error'
+      in
+  let F1 = fun() ->
+         receive PID2 when call 'erlang':'is_pid'(PID2) ->
+                receive X when 'true' -> call 'erlang':'!'(PID2, X)
+                after 'infinity' -> 'error' 
+         after 'infinity' -> 'error'
+      in
+  let F2 = fun() ->
+           receive X when 'true' ->
+                receive Y when 'true' ->
+                    do do call 'io':'fwrite'('first message: ') call 'io':'fwrite'(X)
+                       do call 'io':'fwrite'('second message: ') call 'io':'fwrite'(Y)
+                after 'infinity' -> 'error'
+           after 'infinity' -> 'error'
+      in
+  let PID0 = call 'erlang':'spawn'(F0) in
+  let PID1 = call 'erlang':'spawn'(F1) in
+  let PID2 = call 'erlang':'spawn'(F2) in
+  let A = call 'erlang':'!'(PID0, {PID1, PID2}) in
+    do call 'erlang':'!'(PID1, PID2) 'ok'
+
+'signal_ordering_3'/0 = fun () ->
+  let F = fun() ->
+         receive X when 'true' -> 
+             call 'io':'fwrite'(X)
+         after 'infinity' -> 'error'
+      in
+  let PID0 = call 'erlang':'spawn'(F) in
+  let PID1 = call 'erlang':'spawn'(F) in
+    do call 'erlang':'!'(PID0, 'fst')
+    do call 'erlang':'!'(PID1, 'snd')
+       'ok'
+
+'signal_ordering_4'/0 = fun () ->
+  let F = fun() ->
+         do call 'timer':'sleep'(1)
+         receive X when 'true' -> 
+             call 'io':'fwrite'(X)
+         after 'infinity' -> 'error'
+      in
+  let F0 = fun() ->
+         receive X when 'true' -> 
+             call 'io':'fwrite'(X)
+         after 'infinity' -> 'error'
+      in
+  let PID0 = call 'erlang':'spawn'(F) in
+  let PID1 = call 'erlang':'spawn'(F0) in
+    do call 'erlang':'!'(PID0, 'fst')
+    do call 'erlang':'!'(PID1, 'snd')
+       'ok'
+
+'test_1'/0 = fun () -> 0
+'test_2'/0 = fun () -> 0
+'test_3'/0 = fun () -> 0
+
+%% trapping kill which comes from link
+'test_4'/0 = fun () -> 0
+
+%% kill through link, without traps -> no conversion to killed
+'test_5'/0 = fun () -> 0
+
+%% kill sent explicitly, converted to killed
+'test_6'/0 = fun () -> 0
+
+%% trapping exits
+'test_7'/0 = fun () -> 0
+
+%% explicit exit signal drop
+'test_8'/0 = fun () -> 0
+
+%% implicit exit signal drop 
+'test_9'/0 = fun () -> 0
+
+end

erlang-playground/m.core

@@ -0,0 +1,5 @@
+module 'm' []
+    attributes []
+
+'g'/0 = fun() -> 5
+

src/Bisimulations.v

@@ -10,30 +10,10 @@ Theorem eq_is_strong_bisim :
 Proof.
   split; intros.
   {
-    subst. induction H0.
-    * eexists. split. 2: reflexivity.
-      eapply n_send; try eassumption.
-    * eexists. split. 2: reflexivity.
-      eapply n_arrive; try eassumption.
-    * eexists. split. 2: reflexivity.
-      eapply n_other; try eassumption.
-    * eexists. split. 2: reflexivity.
-      eapply n_spawn; try eassumption.
-    * eexists. split. 2: reflexivity.
-      eapply n_terminate.
+    subst. eexists. split. exact H0. auto.
   }
   {
-    subst. induction H0.
-    * eexists. split. 2: reflexivity.
-      eapply n_send; try eassumption.
-    * eexists. split. 2: reflexivity.
-      eapply n_arrive; try eassumption.
-    * eexists. split. 2: reflexivity.
-      eapply n_other; try eassumption.
-    * eexists. split. 2: reflexivity.
-      eapply n_spawn; try eassumption.
-    * eexists. split. 2: reflexivity.
-      eapply n_terminate.
+    subst. eexists. split. exact H0. auto.
   }
 Qed.
 
@@ -156,12 +136,12 @@ Qed.
 
 Goal forall ether, Node_equivalence (ether, 
                          0 : inl ([], ELet "X"%string (ELit 0%Z) (EVar 0), [], [], false) ||||
-                         1 : inl ([], EConcBIF (ELit "send"%string) [EPid 0;ELit 1%Z], [], [], false) ||||
+                         1 : inl ([], EBIF (ELit "send"%string) [EPid 0;ELit 1%Z], [], [], false) ||||
                          nullpool
                       )
                       (ether,
                         0 : inl ([], ELit 0%Z, [], [], false) ||||
-                        1 : inl ([], EConcBIF (ELit "send"%string) [EPid 0;ELit 1%Z], [], [], false) ||||
+                        1 : inl ([], EBIF (ELit "send"%string) [EPid 0;ELit 1%Z], [], [], false) ||||
                         nullpool
                       ).
 Proof.
@@ -174,3 +154,39 @@ Proof.
       simpl. apply n_refl.
 Qed.
 
+Lemma update_get :
+  forall T x (a : T) f, update x a f x = a.
+Proof.
+  intros. unfold update. now rewrite Nat.eqb_refl.
+Qed.
+
+Lemma any_step_is_not_bisimilar: exists n l,
+  ~weak_bisimulation (fun Π Σ => Π -[ n | l ]ₙ->* Σ).
+Proof.
+  exists 2, [(AInternal, 0); (AInternal, 0)]. intro. destruct H. clear H0.
+  remember (etherAdd 1 0 (Exit (ELit "kill"%string) false) (fun (_ _ : PID) => @nil Signal), 0 : inl ([], ELet "X"%string (ELit 0%Z) (EVar 0), [], [], false) |||| nullpool) as Π.
+  remember (etherAdd 1 0 (Exit (ELit "kill"%string) false) (fun (_ _ : PID) => @nil Signal), 0 : inl ([], ELit 0%Z, [], [], false) |||| nullpool) as Σ.
+  remember (fun (_ _ : PID) => @nil Signal, 0 : inr [] |||| nullpool) as Π'.
+  assert (Π -[ 2 | [(AInternal, 0); (AInternal, 0)] ]ₙ->* Σ) as D1. {
+    subst. econstructor.
+    constructor; auto. do 2 constructor.
+    econstructor. constructor; auto. do 3 constructor.
+    constructor.
+  }
+  assert (Π -[ AArrive 1 0 (Exit (ELit "kill"%string) false) | 0 ]ₙ-> Π') as D2. {
+    subst. constructor. cbn. unfold etherAdd, update. cbn.
+    do 2 f_equal. extensionality x. destruct x; auto.
+    destruct x; auto.
+    extensionality x. destruct x; auto.
+    replace [] with (map (fun x:PID => (x, killed)) []) by auto.
+    apply p_exit_terminate; auto.
+  }
+  specialize (H Π Σ Π' (AArrive 1 0 (Exit (ELit "kill"%string) false)) 0 ltac:(congruence) D1 D2).
+  destruct H as [Σ' [H_1 H_2]].
+  subst. clear D2 D1.
+  inversion H_2; subst.
+  inversion H5; subst. clear H7.
+  apply equal_f with 0 in H0. inversion H0; subst.
+  inversion H1.
+Qed.
+

src/CIU.v

@@ -120,12 +120,12 @@ Theorem CIU_eval : forall e1 v,
   ⟨ [], e1 ⟩ -->* v -> CIU e1 v /\ CIU v e1.
 Proof.
   intros. split. split. 2: split. auto.
-  apply step_any_closedness in H0; auto. 1-2: now constructor.
+  apply step_any_closedness in H0; auto. now constructor.
   intros. destruct H2, H0, H3. eapply frame_indep_nil in H3.
   eapply terminates_step_any. 2: exact H3. eexists. exact H2.
 
   split. 2: split. 2: auto.
-  apply step_any_closedness in H0; auto. 1-2: now constructor.
+  apply step_any_closedness in H0; auto. now constructor.
   intros. destruct H2, H0, H3. eapply frame_indep_nil in H3.
   exists (x + x0).
   eapply term_step_term. exact H3. 2: lia. replace (x + x0 - x0) with x by lia. exact H2.
@@ -161,8 +161,9 @@ Proof.
      - simpl in H23. inversion H23. subst. simpl in H24. eexists; eassumption.
      - apply inf_diverges in H24. contradiction.
   * intros. assert (FSCLOSED (FCase (PCons PVar PVar) (EVar 1) inf :: F)). {
-       constructor; auto. constructor; auto. 2: repeat constructor.
-       simpl. do 2 constructor. auto. inversion H8. inversion H8.
+       constructor; auto. constructor; auto.
+       do 2 constructor.
+       do 2 constructor. auto. intros. inversion H8. inversion H8.
      }
      specialize (H5 (FCase (PCons PVar PVar) (EVar 1) inf :: F) H8).
      destruct H7.