Replace par primitive by fork.

lib/pulse/core/PulseCore.InstantiatedSemantics.fst

@@ -142,7 +142,7 @@ let sub (#a:Type u#a)
 : stt a pre2 post2
 = coerce_eq (conv pre1 pre2 post1 post2 pf1 pf2) e
 
-let par f0 f1 = fun _ -> Sem.par (f0 ()) (f1 ())
+let fork f0 = fun _ -> Sem.fork (f0 ())
 
 let hide_div #a #pre #post (f:unit -> Dv (stt a pre post))
 : stt a pre post

lib/pulse/core/PulseCore.InstantiatedSemantics.fsti

@@ -113,10 +113,8 @@ val sub (#a:Type u#a)
         (e:stt a pre1 post1)
 : stt a pre2 post2
 
-val par (#p0 #q0 #p1 #q1:_)
-        (f0:stt unit p0 (fun _ -> q0))
-        (f1:stt unit p1 (fun _ -> q1))
-: stt unit (p0 ** p1) (fun _ -> q0 ** q1)
+val fork #p0 (f0:stt unit p0 (fun _ -> emp))
+: stt unit p0 (fun _ -> emp)
 
 val hide_div #a #pre #post (f:unit -> Dv (stt a pre post))
 : stt a pre post

lib/pulse/core/PulseCore.Semantics.fst

@@ -42,12 +42,10 @@ let is_unit #a (x:a) (f:a -> a -> a) =
 (**
  * A state typeclass:
  *  - [s] is the type of states
- *  - [is_full_mem] a refinement on states to the entire heap used at runtime
  *  - [pred] is the type of state assertions
  *  - [emp] is the empty state assertion
  *  - [star] is the separating conjunction of state assertions
  *  - [interp p s] is the interpretation of a state assertion [p] in a state [s]
- *  - [evolves] is a preorder on states, constraining how it evolves
  *  - [invariant] is an internal invariant that a caller can instantiate and is maintained
  *                by every action and the semantics as a whole
  *  - [laws] state that {pred, emp, star} are a commutative monoid
@@ -122,7 +120,7 @@ let as_post (#st:state u#s) (#a:Type u#a) (p:st.pred)
  *  pre- and post-conditions so that we can do proofs
  *  intrinsically.
  *
- *  Universe-polymorphic im both the state and result type
+ *  Universe-polymorphic in both the state and result type
  *
  *)
 noeq
@@ -139,17 +137,14 @@ type m (#st:state u#s) : (a:Type u#a) -> st.pred -> post st a -> Type u#(max (ac
       f:action st b ->
       k:(x:b -> Dv (m a (f.post x) post)) ->
       m a f.pre post
-  | Par:
+  | Par: // runs m0 concurrently without waiting for it
       #pre0:_ ->
-      #post0:_ ->
-      m0:m (U.raise_t unit) pre0 (as_post post0) ->
-      #pre1:_ ->
-      #post1:_ ->
-      m1:m (U.raise_t unit) pre1 (as_post post1) ->
-      #a:_ ->
-      #post:_ ->
-      k:m a (st.star post0 post1) post ->
-      m a (st.star pre0 pre1) post
+      m0:m (U.raise_t unit) pre0 (as_post #st st.emp) ->
+      #a:Type u#a ->
+      #pre:_ ->
+      #post:post st a ->
+      k:m a pre post ->
+      m a (pre0 `st.star` pre) post
 
 /// The semantics comes in two levels:
 ///
@@ -201,9 +196,9 @@ let rec step
       weaken (return (Step _ n))
     in
     weaken <| bind (PNST.lift <| (NST.lift <| f.step frame)) k
-  | Par #_ #pre0 #post0 (Ret x0) #pre1 #post1 (Ret x1) #a #post k ->
-    weaken <| return <| Step _ k
-  | Par #_ #pre0 #post0 m0 #pre1 #post1 m1 #a #postk k ->
+  | Par #_ #pre0 (Ret x0) #a #pre #post k ->
+    weaken <| return <| Step pre k
+  | Par #_ #pre0 m0 #a #prek #postk k ->
     let q : post st a = coerce_eq () q in
     let choose (b:bool)
     : pnst_sep st
@@ -212,11 +207,11 @@ let rec step
         (fun x -> (Step?.next x `st.star` frame))
     = if b
       then weaken <| 
-           bind (step m0 (pre1 `st.star` frame))
-                (fun x -> return <| Step _ <| Par (Step?.m x) m1 k)
+           bind (step m0 (prek `st.star` frame))
+                (fun x -> return <| Step _ <| Par (Step?.m x) k)
       else weaken <| 
-           bind (step m1 (pre0 `st.star` frame))
-                (fun x -> return <| Step _ <| Par m0 (Step?.m x) k) 
+           bind (step k (pre0 `st.star` frame))
+                (fun x -> return <| Step _ <| Par m0 (Step?.m x))
     in
     weaken <| bind (lift <| NST.flip()) choose 
 
@@ -303,17 +298,12 @@ let rec mbind
     | Ret x -> g x
     | Act act k ->
       Act act (fun x -> mbind (k x) g)
-    | Par #_ #pre0 #post0 ml
-             #pre1 #post1 mr
-             #postk k ->
-      let k : m b (post0 `st.star` post1) r = mbind k g in
-      let ml' : m (U.raise_t u#0 u#b unit) pre0 (as_post post0) =
-         mbind ml (fun _ -> Ret #_ #(U.raise_t u#0 u#b unit) #(as_post post0) (U.raise_val u#0 u#b ()))
-      in
-      let mr' : m (U.raise_t u#0 u#b unit) pre1 (as_post post1) =
-         mbind mr (fun _ -> Ret #_ #(U.raise_t u#0 u#b unit) #(as_post post1) (U.raise_val u#0 u#b ()))
+    | Par #_ #pre0 ml #_ #prek #postk k ->
+      let k : m b prek r = mbind k g in
+      let ml' : m (U.raise_t u#0 u#b unit) pre0 (as_post st.emp) =
+         mbind ml (fun _ -> Ret #_ #(U.raise_t u#0 u#b unit) #(as_post st.emp) (U.raise_val u#0 u#b ()))
       in
-      Par ml' mr' k
+      Par ml' k
 
 let act_as_m0
     (#st:state u#s)
@@ -401,29 +391,19 @@ let rec frame (#st:state u#s)
      | Ret x -> Ret x
      | Act f k ->
        Act (frame_action f fr) (fun x -> frame fr (k x))
-     | Par #_ #pre0 #post0 m0 #pre1 #post1 m1 #postk k ->
-       let m0'
-         : m (U.raise_t u#0 u#a unit) (pre0 `st.star` fr) 
-             (F.on_dom _ (fun x -> (as_post post0) x `st.star` fr))
-         = frame fr m0 in
-       let m0'
-         : m (U.raise_t u#0 u#a unit) (pre0 `st.star` fr) (as_post (post0 `st.star` fr))
-         = m0'
-       in
+     | Par #_ #pre0 m0 #_ #prek #postk k ->
        let k' = frame fr k in
-       Par m0' m1 k'
+       Par m0 k'
 
 (**
- * [par]: Parallel composition
+ * [fork]: Parallel execution using fork
  * Works by just using the `Par` node and `Ret` as its continuation
  **)
-let par (#st:state u#s)
-        #p0 #q0 (m0:m unit p0 (as_post q0))
-        #p1 #q1 (m1:m unit p1 (as_post q1))
- : Dv (m u#s u#0 u#act unit (p0 `st.star` p1) (as_post (q0 `st.star` q1)))
- = let m0' = mbind m0 (fun _ -> Ret #_ #_ #(as_post q0) (U.raise_val u#0 u#0 ())) in
-   let m1' = mbind m1 (fun _ -> Ret #_ #_ #(as_post q1) (U.raise_val u#0 u#0 ())) in
-   Par m0' m1' (Ret ())
+let fork (#st:state u#s)
+        #p0 (m0:m unit p0 (as_post st.emp))
+ : Dv (m u#s u#0 u#act unit p0 (as_post st.emp))
+ = let m0' = mbind m0 (fun _ -> Ret #st #_ #(as_post st.emp) (U.raise_val ())) in
+   Par m0' (Ret ())
 
 let conv (#st:state u#s) (a:Type u#a)
          (#p:st.pred)

lib/pulse/lib/Pulse.Lib.Core.fst

@@ -161,7 +161,7 @@ let stt = I.stt
 let return_stt_noeq = I.return
 let bind_stt = I.bind
 let frame_stt = I.frame
-let par_stt = I.par
+let fork f = I.fork (f ())
 let sub_stt = I.sub
 let conv_stt pf1 pf2 = I.conv #_ _ _ _ _ pf1 pf2
 let hide_div = I.hide_div

lib/pulse/lib/Pulse.Lib.Core.fsti

@@ -229,16 +229,10 @@ val frame_stt
   (e:stt a pre post)
 : stt a (pre ** frame) (fun x -> post x ** frame)
 
-val par_stt
-  (#preL:slprop)
-  (#postL:slprop) 
-  (#preR:slprop)
-  (#postR:slprop)
-  (f:stt unit preL (fun _ -> postL))
-  (g:stt unit preR (fun _ -> postR))
-: stt unit
-      (preL ** preR)
-      (fun _ -> postL ** postR)
+val fork
+  (#pre:slprop)
+  (f:unit -> stt unit pre (fun _ -> emp))
+: stt unit pre (fun _ -> emp)
 
 val sub_stt (#a:Type u#a)
             (#pre1:slprop)

lib/pulse/lib/Pulse.Lib.Par.fst

@@ -0,0 +1,41 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module Pulse.Lib.Par
+open Pulse.Lib.Core
+open Pulse.Lib.ConditionVar
+
+#lang-pulse
+
+fn par_stt' #preL #postL #preR #postR
+  (f:unit -> stt unit preL (fun _ -> postL))
+  (g:unit -> stt unit preR (fun _ -> postR))
+  requires preL ** preR
+  ensures postL ** postR
+{
+  let c = create postL;
+  fn auxL ()
+    requires preL ** send c postL
+    ensures emp
+  {
+    f ();
+    signal c #postL;
+  };
+  fork auxL;
+  g ();
+  wait c #postL;
+}
+
+let par_stt f g = par_stt' (fun _ -> f) (fun _ -> g)

lib/pulse/lib/Pulse.Lib.Par.fsti

@@ -0,0 +1,28 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module Pulse.Lib.Par
+open Pulse.Lib.Core
+
+val par_stt
+  (#preL:slprop)
+  (#postL:slprop)
+  (#preR:slprop)
+  (#postR:slprop)
+  (f:stt unit preL (fun _ -> postL))
+  (g:stt unit preR (fun _ -> postR))
+: stt unit
+      (preL ** preR)
+      (fun _ -> postL ** postR)

lib/pulse/lib/Pulse.Lib.Task.fst

@@ -1437,21 +1437,21 @@ fn gather_alive
   fold (pool_alive #f p);
 }
 
-
-(* Very basic model of a thread fork *)
-assume
-val fork
-  (#p #q : slprop)
-  (f : unit -> stt unit p (fun _ -> q))
-  : stt unit p (fun _ -> emp)
+fn worker_thread (#f:perm) (p : pool)
+  requires pool_alive #f p
+  ensures emp
+{
+  worker p;
+  drop_ (pool_alive #f p)
+}
 
 fn spawn_worker
   (p:pool)
   (#f:perm)
   requires pool_alive #f p
   ensures  emp
 {
-  fork (fun () -> worker #f p)
+  fork (fun () -> worker_thread #f p)
 }
 
 fn rec spawn_workers

src/checker/Pulse.Reflection.Util.fst

@@ -577,7 +577,7 @@ let mk_sub_stt_ghost (u:R.universe) (a pre1 pre2 post1 post2 e:R.term)  =
 
 let mk_par (u:R.universe) (aL aR preL postL preR postR eL eR:R.term) =
   let open R in
-  let lid = mk_pulse_lib_core_lid "par_stt" in
+  let lid = ["Pulse"; "Lib"; "Par"; "par_stt"] in
   let t = pack_ln (Tv_UInst (R.pack_fv lid) [u]) in
   let t = pack_ln (Tv_App t (aL, Q_Implicit)) in
   let t = pack_ln (Tv_App t (aR, Q_Implicit)) in