Mutex guard based Mutex API

lib/pulse/lib/Pulse.Lib.Mutex.fst

@@ -20,6 +20,7 @@ open Pulse.Lib.Core
 open Pulse.Lib.Reference
 open Pulse.Lib.SpinLock
 
+module R = Pulse.Lib.Reference
 module B = Pulse.Lib.Box
 
 open Pulse.Main
@@ -30,12 +31,20 @@ type mutex (a:Type0) : Type0 = {
   l:lock;
 }
 
+let mutex_guard a = R.ref a
+
 let lock_inv (#a:Type0) (r:B.box a) (v:a -> vprop)
   : (w:vprop { (forall x. is_big (v x)) ==> is_big w }) =
   exists* x. B.pts_to r x ** v x
 
 let mutex_live #a m #p v = lock_alive m.l #p (lock_inv m.r v)
 
+let pts_to mg #p x = R.pts_to mg #p x
+
+let op_Bang #a mg #x #p = R.op_Bang #a mg #x #p
+let op_Colon_Equals #a r y #x = R.op_Colon_Equals #a r y #x
+let replace #a r y #x = R.replace #a r y #x
+
 ```pulse
 fn new_mutex' (#a:Type0) (v:a -> vprop { forall x. is_big (v x) }) (x:a)
   requires v x
@@ -55,35 +64,37 @@ fn new_mutex' (#a:Type0) (v:a -> vprop { forall x. is_big (v x) }) (x:a)
 
 let new_mutex = new_mutex'
 
-let belongs_to_mutex (#a:Type0) (r:ref a) (m:mutex a) : vprop =
+let belongs_to (#a:Type0) (r:mutex_guard a) (m:mutex a) : vprop =
   pure (r == B.box_to_ref m.r) ** lock_acquired m.l
 
 ```pulse
 fn lock' (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a)
   requires mutex_live m #p v
-  returns r:ref a
-  ensures mutex_live m #p v ** r `belongs_to_mutex` m ** (exists* x. pts_to r x ** v x)
+  returns r:mutex_guard a
+  ensures mutex_live m #p v ** r `belongs_to` m ** (exists* x. pts_to r x ** v x)
 {
   unfold (mutex_live m#p v);
   acquire m.l;
   unfold lock_inv;
-  fold (belongs_to_mutex (B.box_to_ref m.r) m);
+  fold (belongs_to (B.box_to_ref m.r) m);
   fold (mutex_live m #p v);
   B.to_ref_pts_to m.r;
+  with _x. rewrite (R.pts_to (B.box_to_ref m.r) _x) as
+                   (pts_to (B.box_to_ref m.r) _x);
   B.box_to_ref m.r
 } 
 ```
 
 let lock = lock'
 
 ```pulse
-fn unlock' (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a) (r:ref a)
-  requires mutex_live m #p v ** r `belongs_to_mutex` m ** (exists* x. pts_to r x ** v x)
+fn unlock' (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a) (mg:mutex_guard a)
+  requires mutex_live m #p v ** mg `belongs_to` m ** (exists* x. pts_to mg x ** v x)
   ensures mutex_live m #p v
 {
   unfold (mutex_live m #p v);
-  unfold (r `belongs_to_mutex` m);
-  with x. rewrite (pts_to r x) as (pts_to (B.box_to_ref m.r) x);
+  unfold (mg `belongs_to` m);
+  with x. rewrite (pts_to mg x) as (R.pts_to (B.box_to_ref m.r) x);
   B.to_box_pts_to m.r;
   fold lock_inv;
   release m.l;

lib/pulse/lib/Pulse.Lib.Mutex.fsti

@@ -24,36 +24,53 @@ module T = FStar.Tactics.V2
 // A model of Rust mutex
 //
 
-//
-// Can we make the specs more precise? E.g., log the values in an append-only log
-//   and say that at the time of locking the box value appears later than any (stable) snapshot
-//   of the log?
-//
-
 val mutex (a:Type0) : Type0
 
+val mutex_guard (a:Type0) : Type0
+
 val mutex_live
   (#a:Type0)
   (m:mutex a)
   (#[T.exact (`1.0R)] p:perm)
   (v:a -> vprop)  : vprop
 
+//
+// mutex_guard is a ref-like type
+//
+
+val pts_to (#a:Type0) (mg:mutex_guard a) (#[T.exact (`1.0R)] p:perm) (x:a) : vprop
+
+val ( ! ) (#a:Type0) (mg:mutex_guard a) (#x:erased a) (#p:perm)
+  : stt a
+      (requires pts_to mg #p x)
+      (ensures fun y -> pts_to mg #p x ** pure (reveal x == y))
+
+val ( := ) (#a:Type0) (mg:mutex_guard a) (y:a) (#x:erased a)
+  : stt unit
+      (requires mg `pts_to` x)
+      (ensures fun _ -> mg `pts_to` y)
+
+val replace (#a:Type0) (mg:mutex_guard a) (y:a) (#x:erased a)
+  : stt a
+      (requires mg `pts_to` x)
+      (ensures fun r -> mg `pts_to` y ** pure (r == reveal x))
+
 val new_mutex (#a:Type0) (v:a -> vprop { forall x. is_big (v x) }) (x:a)
   : stt (mutex a)
-        (requires v x)
-        (ensures fun m -> mutex_live m v)
+      (requires v x)
+      (ensures fun m -> mutex_live m v)
 
-val belongs_to_mutex (#a:Type0) (r:ref a) (m:mutex a) : vprop
+val belongs_to (#a:Type0) (mg:mutex_guard a) (m:mutex a) : vprop
 
 val lock (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a)
-  : stt (ref a)
-        (requires mutex_live m #p v)
-        (ensures fun r -> mutex_live m #p v ** r `belongs_to_mutex` m ** (exists* x. pts_to r x ** v x))
+  : stt (mutex_guard a)
+      (requires mutex_live m #p v)
+      (ensures fun mg -> mutex_live m #p v ** mg `belongs_to` m ** (exists* x. pts_to mg x ** v x))
 
-val unlock (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a) (r:ref a)
+val unlock (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a) (mg:mutex_guard a)
   : stt unit
-        (requires mutex_live m #p v ** r `belongs_to_mutex` m ** (exists* x. pts_to r x ** v x))
-        (ensures fun _ -> mutex_live m #p v)
+      (requires mutex_live m #p v ** mg `belongs_to` m ** (exists* x. pts_to mg x ** v x))
+      (ensures fun _ -> mutex_live m #p v)
 
 val share (#a:Type0) (#v:a -> vprop) (#p:perm) (m:mutex a)
   : stt_ghost unit emp_inames

pulse2rust/src/Pulse2Rust.Extract.fst

@@ -91,8 +91,6 @@ let type_of (g:env) (e:expr) : bool =  // is_mut
 
   | _ -> false
 
-  // | _ -> fail_nyi (format1 "type_of %s" (expr_to_string e))
-
 //
 // rust functions are uncurried
 //
@@ -418,7 +416,8 @@ let rec lb_init_and_def (g:env) (lb:S.mllb)
       match lb.mllb_def.expr with
       | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, _) ->
         S.string_of_mlpath p = "Pulse.Lib.Vec.alloc" ||
-        S.string_of_mlpath p = "Pulse.Lib.Box.alloc"
+        S.string_of_mlpath p = "Pulse.Lib.Box.alloc" ||
+        S.string_of_mlpath p = "Pulse.Lib.Mutex.lock"
       | _ -> false in
     is_mut,
     lb.mllb_tysc |> must |> snd |> extract_mlty g,
@@ -473,20 +472,25 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr =
 
   | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, [e1; e2; _])
     when S.string_of_mlpath p = "Pulse.Lib.Reference.op_Colon_Equals" ||
-         S.string_of_mlpath p = "Pulse.Lib.Box.op_Colon_Equals" ->
+         S.string_of_mlpath p = "Pulse.Lib.Box.op_Colon_Equals" ||
+         S.string_of_mlpath p = "Pulse.Lib.Mutex.op_Colon_Equals" ->
     let e1 = extract_mlexpr g e1 in
     let e2 = extract_mlexpr g e2 in
     let b = type_of g e1 in
-    if b
-    then mk_assign e1 e2
-    else mk_ref_assign e1 e2
+    let is_mutex_guard = S.string_of_mlpath p = "Pulse.Lib.Mutex.op_Colon_Equals" in
+    if is_mutex_guard || not b
+    then mk_ref_assign e1 e2
+    else mk_assign e1 e2
   | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, [e; _; _])
     when S.string_of_mlpath p = "Pulse.Lib.Reference.op_Bang" ||
-         S.string_of_mlpath p = "Pulse.Lib.Box.op_Bang" ->
+         S.string_of_mlpath p = "Pulse.Lib.Box.op_Bang" ||
+         S.string_of_mlpath p = "Pulse.Lib.Mutex.op_Bang" ->
     let e = extract_mlexpr g e in
     let b = type_of g e in
-    if b then e
-    else mk_ref_read e
+    let is_mutex_guard = S.string_of_mlpath p = "Pulse.Lib.Mutex.op_Colon_Equals" in
+    if is_mutex_guard || not b
+    then mk_ref_read e
+    else e
 
   | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, _)}, [e1; e2; _])
     when S.string_of_mlpath p = "Pulse.Lib.Pervasives.ref_apply" ->
@@ -528,20 +532,24 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr =
     let e3 = extract_mlexpr g e3 in
     mk_assign (mk_expr_index e1 e2) e3
 
-  | S.MLE_App ({ expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e_v::e_i::e_x::_)
+  | S.MLE_App ({ expr=S.MLE_TApp ({expr=S.MLE_Name p}, [a])}, e_v::e_i::e_x::_)
     when S.string_of_mlpath p = "Pulse.Lib.Vec.replace_i" ||
          S.string_of_mlpath p = "Pulse.Lib.Vec.replace_i_ref" ->
 
     let e_v = extract_mlexpr g e_v in
     let e_i = extract_mlexpr g e_i in
     let e_x = extract_mlexpr g e_x in
     let is_mut = true in
-    mk_mem_replace (mk_reference_expr is_mut (mk_expr_index e_v e_i)) e_x
+    mk_mem_replace (extract_mlty g a)
+                   (mk_reference_expr is_mut (mk_expr_index e_v e_i)) e_x
 
-  | S.MLE_App ({ expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e_r::e_x::_)
+  | S.MLE_App ({ expr=S.MLE_TApp ({expr=S.MLE_Name p}, [a])}, e_r::e_x::_)
     when S.string_of_mlpath p = "Pulse.Lib.Reference.replace" ->
-
-    mk_mem_replace (extract_mlexpr g e_r) (extract_mlexpr g e_x)
+
+    mk_mem_replace (extract_mlty g a)
+                   (extract_mlexpr g e_r)
+                   (extract_mlexpr g e_x)
+
 
     //
     // vec_as_array e extracted to &mut e
@@ -580,6 +588,18 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr =
     when S.string_of_mlpath p = "Pulse.Lib.Mutex.lock" ->
     let e = extract_mlexpr g e in
     mk_lock_mutex e
+  | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, _::_::_::e::_)
+    when S.string_of_mlpath p = "Pulse.Lib.Mutex.unlock" ->
+    let e = extract_mlexpr g e in
+    mk_unlock_mutex e
+  | S.MLE_App ({ expr=S.MLE_TApp ({expr=S.MLE_Name p}, [a])}, e_mg::e_x::_)
+    when S.string_of_mlpath p = "Pulse.Lib.Mutex.replace" ->
+
+    let is_mut = true in
+    mk_mem_replace (extract_mlty g a)
+                   (mk_reference_expr is_mut (extract_mlexpr g e_mg))
+                   (extract_mlexpr g e_x)
+
 
   | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, [e1; e2])
     when S.string_of_mlpath p = "Pulse.Lib.Array.Core.free" ->
@@ -680,29 +700,18 @@ and extract_mlexpr_to_stmts (g:env) (e:S.mlexpr) : list stmt =
 
   | S.MLE_Let ((S.NonRec, [lb]), e) ->
     begin
-      match lb.mllb_def.expr with
-      | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, _)}, _)
-        when S.mlpath_to_string p = "Pulse.Lib.Mutex.unlock" ->
-        extract_mlexpr_to_stmts g e
-      | _ ->
-        let is_mut, ty, init = lb_init_and_def g lb in
-        let topt =
-          match lb.mllb_def.expr with
-          | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, _::e::_)
-            when S.string_of_mlpath p = "Pulse.Lib.Mutex.lock" ->
-            Some ty
-          | _ -> None in 
-        let s = mk_local_stmt
-          (match lb.mllb_tysc with
-           | Some (_, S.MLTY_Erased) -> None
-           | _ -> Some (varname lb.mllb_name))
-          topt
-          is_mut
-          init in
-        s::(extract_mlexpr_to_stmts (push_local g lb.mllb_name ty is_mut) e)
+      let is_mut, ty, init = lb_init_and_def g lb in
+      let topt = None in
+      let s = mk_local_stmt
+        (match lb.mllb_tysc with
+         | Some (_, S.MLTY_Erased) -> None
+         | _ -> Some (varname lb.mllb_name))
+        topt
+        is_mut
+        init in
+      s::(extract_mlexpr_to_stmts (push_local g lb.mllb_name ty is_mut) e)
     end
 
-
   | S.MLE_App ({ expr=S.MLE_TApp ({ expr=S.MLE_Name p }, _) }, _)
     when S.string_of_mlpath p = "failwith" ->
     [Stmt_expr (mk_call (mk_expr_path_singl panic_fn) [])]

pulse2rust/src/Pulse2Rust.Rust.Syntax.fst

@@ -169,9 +169,11 @@ let mk_expr_struct (path:list string) (fields:list (string & expr)) : expr =
 
 let mk_expr_tuple (l:list expr) : expr = Expr_tuple l
 
-let mk_mem_replace (e:expr) (new_v:expr) : expr =
+let mk_mem_replace (t:typ) (e:expr) (new_v:expr) : expr =
   mk_call
-    (mk_expr_path ["std"; "mem"; "replace"])
+    (Expr_path [{ path_segment_name = "std"; path_segment_generic_args = [] };
+                { path_segment_name = "mem"; path_segment_generic_args = [] };
+                { path_segment_name = "replace"; path_segment_generic_args = [t] }])
     [e; new_v]
 
 let mk_method_call (receiver:expr) (name:string) (args:list expr) : expr =
@@ -188,9 +190,14 @@ let mk_new_mutex (e:expr) =
 
 let mk_lock_mutex (e:expr) : expr =
   let e_lock = mk_method_call e "lock" [] in
-  let e_lock_unwrap = mk_method_call e_lock "unwrap" [] in
-  let is_mut = true in
-  mk_reference_expr is_mut e_lock_unwrap
+  mk_method_call e_lock "unwrap" []
+  // let is_mut = true in
+  // mk_reference_expr is_mut e_lock_unwrap
+
+let mk_unlock_mutex (e:expr) : expr =
+  mk_call
+    (mk_expr_path ["std"; "mem"; "drop"])
+    [e]
 
 let mk_scalar_fn_arg (name:string) (is_mut:bool) (t:typ) =
   Fn_arg_pat {

pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti

@@ -345,11 +345,12 @@ val mk_expr_field (base:expr) (f:string) : expr
 val mk_expr_field_unnamed (base:expr) (i:int) : expr
 val mk_expr_struct (path:list string) (fields:list (string & expr)) : expr
 val mk_expr_tuple (l:list expr) : expr
-val mk_mem_replace (e:expr) (new_v:expr) : expr
+val mk_mem_replace (t:typ) (e:expr) (new_v:expr) : expr
 val mk_method_call (receiver:expr) (name:string) (args:list expr) : expr
 
 val mk_new_mutex (e:expr) : expr
 val mk_lock_mutex (e:expr) : expr
+val mk_unlock_mutex (e:expr) : expr
 
 val mk_local_stmt (name:option string) (t:option typ) (is_mut:bool) (init:expr) : stmt
 val mk_scalar_fn_arg (name:string) (is_mut:bool) (t:typ) : fn_arg