Merge pull request #2 from mtzguido/misc

Misc changes to task pool

share/pulse/examples/parix/TaskPool.fsti → lib/pulse/lib/Pulse.Lib.Task.fsti

@@ -14,10 +14,9 @@
    limitations under the License.
 *)
 
-module TaskPool
+module Pulse.Lib.Task
 
 open Pulse.Lib.Pervasives
-open Pulse.Lib.SpinLock
 open Pulse.Lib.Par.Pledge
 module T = FStar.Tactics
 
@@ -109,6 +108,8 @@ val teardown_pool
   (p:pool)
   : stt unit (pool_alive #full_perm p) (fun _ -> pool_done p)
 
+(* Or, have at least an epsilon of permission over it, and know that
+the rest of it (1-e) is "sunk" into the pool itself. *)
 val teardown_pool'
   (#is : Pulse.Lib.InvList.invlist)
   (p:pool) (f:perm{f `lesser_perm` full_perm})

share/pulse/examples/MSort.fst → share/pulse/examples/MSort.Base.fst

@@ -1,4 +1,4 @@
-module MSort
+module MSort.Base
 
 open FStar.Ghost
 open Pulse.Lib.Pervasives
@@ -7,7 +7,6 @@ module S = FStar.Seq
 module SZ = FStar.SizeT
 open MSort.SeqLemmas
 
-
 #set-options "--z3rlimit 20"
 
 ```pulse
@@ -180,35 +179,3 @@ merge_impl
   A.free sw2;
 }
 ```
-
-
-```pulse
-fn
-rec
-msort
-  (a : array int)
-  (lo hi : SZ.t)
-  (s : erased (S.seq int))
-  requires pts_to_range a (SZ.v lo) (SZ.v hi) (reveal s)
-  ensures  pts_to_range a (SZ.v lo) (SZ.v hi) (sort (reveal s))
-{
-  pts_to_range_prop a;
-  if ((hi `SZ.sub` lo) `SZ.lt` 2sz) {
-    pts_to_range_prop a;
-    singl_is_sorted s;
-    ()
-  } else {
-    let mid : SZ.t = lo `SZ.add` ((hi `SZ.sub` lo) `SZ.div` 2sz);
-
-    pts_to_range_split a (SZ.v lo) (SZ.v mid) (SZ.v hi);
-
-    with s1. assert (pts_to_range a (SZ.v lo) (SZ.v mid) s1);
-    with s2. assert (pts_to_range a (SZ.v mid) (SZ.v hi) s2);
-
-    msort a lo mid s1;
-    msort a mid hi s2;
-
-    merge_impl a lo mid hi () (sort s1) (sort s2);
-  }
-}
-```

share/pulse/examples/MSort.Parallel.fst

@@ -0,0 +1,43 @@
+module MSort.Parallel
+
+open Pulse.Lib.Pervasives
+module S = FStar.Seq
+module SZ = FStar.SizeT
+open MSort.SeqLemmas
+open MSort.Base
+
+```pulse
+fn
+rec
+msort
+  (a : array int)
+  (lo hi : SZ.t)
+  (s : erased (S.seq int))
+  requires pts_to_range a (SZ.v lo) (SZ.v hi) (reveal s)
+  ensures  pts_to_range a (SZ.v lo) (SZ.v hi) (sort (reveal s))
+{
+  pts_to_range_prop a;
+  if ((hi `SZ.sub` lo) `SZ.lt` 2sz) {
+    pts_to_range_prop a;
+    singl_is_sorted s;
+    ()
+  } else {
+    let mid : SZ.t = lo `SZ.add` ((hi `SZ.sub` lo) `SZ.div` 2sz);
+
+    pts_to_range_split a (SZ.v lo) (SZ.v mid) (SZ.v hi);
+
+    with s1. assert (pts_to_range a (SZ.v lo) (SZ.v mid) s1);
+    with s2. assert (pts_to_range a (SZ.v mid) (SZ.v hi) s2);
+
+    parallel
+      requires pts_to_range a (SZ.v lo) (SZ.v mid) (reveal s1)
+           and pts_to_range a (SZ.v mid) (SZ.v hi) (reveal s2)
+      ensures  pts_to_range a (SZ.v lo) (SZ.v mid) (sort (reveal s1))
+          and  pts_to_range a (SZ.v mid) (SZ.v hi) (sort (reveal s2))
+    { msort a lo mid s1; }
+    { msort a mid hi s2; };
+
+    merge_impl a lo mid hi () (sort s1) (sort s2);
+  }
+}
+```

share/pulse/examples/MSort.Sequential.fst

@@ -0,0 +1,36 @@
+module MSort.Sequential
+
+open Pulse.Lib.Pervasives
+module S = FStar.Seq
+module SZ = FStar.SizeT
+open MSort.SeqLemmas
+open MSort.Base
+
+```pulse
+fn rec msort
+  (a : array int)
+  (lo hi : SZ.t)
+  (s : erased (S.seq int))
+  requires pts_to_range a (SZ.v lo) (SZ.v hi) (reveal s)
+  ensures  pts_to_range a (SZ.v lo) (SZ.v hi) (sort (reveal s))
+{
+  pts_to_range_prop a;
+  if ((hi `SZ.sub` lo) `SZ.lt` 2sz) {
+    pts_to_range_prop a;
+    singl_is_sorted s;
+    ()
+  } else {
+    let mid : SZ.t = lo `SZ.add` ((hi `SZ.sub` lo) `SZ.div` 2sz);
+
+    pts_to_range_split a (SZ.v lo) (SZ.v mid) (SZ.v hi);
+
+    with s1. assert (pts_to_range a (SZ.v lo) (SZ.v mid) s1);
+    with s2. assert (pts_to_range a (SZ.v mid) (SZ.v hi) s2);
+
+    msort a lo mid s1;
+    msort a mid hi s2;
+
+    merge_impl a lo mid hi () (sort s1) (sort s2);
+  }
+}
+```

share/pulse/examples/MSortPar.fst → share/pulse/examples/MSort.Task.fst

@@ -1,20 +1,14 @@
-module MSortPar
+module MSort.Task
 
-open FStar.Ghost
 open Pulse.Lib.Pervasives
-module A = Pulse.Lib.Array
 module S = FStar.Seq
 module SZ = FStar.SizeT
-
-open MSort
 open MSort.SeqLemmas
-open TaskPool
-open Pulse.Lib.Par.Pledge
+open MSort.Base
+open Pulse.Lib.Task
 
 ```pulse
-fn
-rec
-t_msort_par
+fn rec t_msort_par
   (p : pool)
   (f : perm)
   (a : array int)
@@ -48,3 +42,21 @@ t_msort_par
   }
 }
 ```
+
+```pulse
+fn rec msort
+  (nthr : pos)
+  (a : array int)
+  (lo hi : SZ.t)
+  (s : erased (S.seq int))
+  requires pts_to_range a (SZ.v lo) (SZ.v hi) (reveal s)
+  ensures  pts_to_range a (SZ.v lo) (SZ.v hi) (sort (reveal s))
+{
+  // No need for pledge reasoning here as t_msort_par is synchronous, even
+  // if it parallelizes internally.
+  let p = setup_pool nthr;
+  t_msort_par p full_perm a lo hi s;
+  teardown_pool p;
+  drop_ (pool_done p);
+}
+```

share/pulse/examples/PledgeArith.fst

@@ -4,7 +4,7 @@ module PledgeArith
 
 open Pulse.Lib.Pervasives
 open Pulse.Lib.InvList
-module T = TaskPool
+module T = Pulse.Lib.Task
 open Pulse.Lib.Par.Pledge
 
 ```pulse

share/pulse/examples/Quicksort.Task.fst

@@ -23,14 +23,10 @@ module SZ = FStar.SizeT
 
 open Pulse.Lib.InvList
 
-module T = TaskPool
+module T = Pulse.Lib.Task
 open Quicksort.Base
 open Pulse.Lib.Par.Pledge
 
-
-let quicksort_pre a lo hi s0 lb rb : vprop =
-  A.pts_to_range a lo hi s0 ** pure (pure_pre_quicksort a lo hi lb rb s0)
-
 let quicksort_post a lo hi s0 lb rb : vprop =
   exists* s. (A.pts_to_range a lo hi s ** pure (pure_post_quicksort a lo hi lb rb s0 s))
 
@@ -63,8 +59,8 @@ fn rec t_quicksort
     T.share_alive p f;
     T.share_alive p (half_perm f);
 
-    t_quicksort p (half_perm (half_perm f)) a r._2 hi pivot rb;
     T.spawn_ p #(half_perm f) (fun () -> t_quicksort p (half_perm (half_perm f)) a lo r._1 lb pivot);
+    t_quicksort p (half_perm (half_perm f)) a r._2 hi pivot rb;
 
     return_pledge [] (T.pool_done p) (T.pool_alive #(half_perm f) p ** A.pts_to_range a r._1 r._2 s2);
     squash_pledge _ _ _;

share/pulse/examples/parix/ParallelFor.fst

@@ -18,7 +18,7 @@ module ParallelFor
 
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Fixpoints
-open TaskPool
+open Pulse.Lib.Task
 open FStar.Real
 open Pulse.Lib.Par.Pledge
 open Pulse.Lib.InvList
@@ -238,18 +238,6 @@ assume val unfrac_n (n:pos) (p:pool) (e:perm)
   : stt unit (range (fun i -> pool_alive #(div_perm e n) p) 0 n)
              (fun () -> pool_alive #e p)
 
-#set-options "--print_implicits --print_universes"
-
-// FIXME: arguments with defaults (i.e. metaargs with tactics)
-// make functions not be recognized by Pulse
-val gspawn_
-  (#pre #post : _)
-  (#e : perm)
-  (p:pool) (f : unit -> stt unit pre (fun _ -> post))
-  : stt unit (pool_alive #e p ** pre)
-             (fun prom -> pool_alive #e p ** pledge [] (pool_done p) post)
-let gspawn_ p f = TaskPool.spawn_ p f
-
 ```pulse
 fn spawned_f_i 
   (p:pool)
@@ -261,7 +249,7 @@ fn spawned_f_i
   requires emp ** (pre i ** pool_alive #e p)
   ensures emp ** (pledge [] (pool_done p) (post i) ** pool_alive #e p)
 {
-  gspawn_ #(pre i) #(post i) #e p (fun () -> f i)
+  spawn_ #(pre i) #(post i) p #e (fun () -> f i)
 }
 ```
 
@@ -351,7 +339,7 @@ fn spawned_f_i_alt
   requires pool_alive p ** pre i
   ensures pool_alive p ** pledge [] (pool_done p) (post i)
 {
-  gspawn_ #(pre i) #(post i) #full_perm p (fun () -> f i)
+  spawn_ #(pre i) #(post i) p #full_perm (fun () -> f i)
 }
 ```
 
@@ -555,16 +543,16 @@ fn h_for_task
 
     p_split pre lo mid hi ();
 
-    gspawn_ #(pool_alive #(half_perm (half_perm e)) p ** range pre lo mid)
+    spawn_ #(pool_alive #(half_perm (half_perm e)) p ** range pre lo mid)
             #(pledge [] (pool_done p) (range post lo mid))
-            #(half_perm e)
             p
+            #(half_perm e)
             (h_for_task__ p (half_perm (half_perm e)) pre post f lo mid);
 
-    gspawn_ #(pool_alive #(half_perm (half_perm e)) p ** range pre mid hi)
+    spawn_ #(pool_alive #(half_perm (half_perm e)) p ** range pre mid hi)
             #(pledge [] (pool_done p) (range post mid hi))
-            #(half_perm e)
             p
+            #(half_perm e)
             (h_for_task__ p (half_perm (half_perm e)) pre post f mid hi);
 
     (* We get this complicated pledge [] from the spawns above. We can
@@ -625,10 +613,10 @@ parallel_for_hier
     assert (pool_alive #one_half p ** pool_alive #one_half p);
 
 
-    gspawn_ #(pool_alive #one_half p ** range pre 0 n)
+    spawn_ #(pool_alive #one_half p ** range pre 0 n)
             #(pledge [] (pool_done p) (range post 0 n))
-            #one_half
             p
+            #one_half
             (h_for_task p one_half pre post f 0 n);
 
     (* We get this complicated pledge [] from the spawn above. We can

share/pulse/examples/parix/TaskPool.Examples.fst

@@ -18,7 +18,7 @@ module TaskPool.Examples
 
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Par.Pledge
-open TaskPool
+open Pulse.Lib.Task
 
 assume
 val qsv : nat -> vprop