Rename NuPool to Pulse.Lib.Task

share/pulse/examples/NuPool.fst → lib/pulse/lib/Pulse.Lib.Task.fst

@@ -14,7 +14,7 @@
    limitations under the License.
 *)
 
-module NuPool
+module Pulse.Lib.Task
 #lang-pulse
 
 open Pulse.Lib.Pervasives

lib/pulse/lib/Pulse.Lib.Task.fsti

@@ -1,5 +1,5 @@
 (*
-   Copyright 2023 Microsoft Research
+   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.
@@ -15,105 +15,85 @@
 *)
 
 module Pulse.Lib.Task
+#lang-pulse
 
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Pledge
-module T = FStar.Tactics
+module T = FStar.Tactics.V2
 
+val handle : Type0
 val pool : Type0
-val pool_alive : (#[T.exact (`1.0R)]p : perm) -> pool -> slprop
-val pool_done : pool -> slprop
-
-val setup_pool (n:pos)
-  : stt pool emp (fun p -> pool_alive #1.0R p)
-
-val task_handle : pool -> a:Type0 -> (a -> slprop) -> Type0
-val joinable : #p:pool -> #a:Type0 -> #post:_ -> th:(task_handle p a post) -> slprop
-val joined   : #p:pool -> #a:Type0 -> #post:_ -> th:(task_handle p a post) -> slprop
-
-val handle_solved
-  (#p : pool) 
-  (#a : Type0)
-  (#post : a -> slprop)
-  (th : task_handle p a post)
-  : slprop
-
-(* NOTE! Spawn only requires an *epsilon* of permission over the pool.
-We do not have to be exclusive owners of it in order to queue a job,
-even if that modifies it. How to model this under the hood? *)
-val spawn
-  (#a : Type0)
-  (#pre : slprop) (#post : a -> slprop)
-  (p : pool)
-  (#[T.exact (`1.0R)] e : perm)
-  ($f : unit -> stt a pre (fun (x:a) -> post x))
-  : stt (task_handle p a post)
-        (pool_alive #e p ** pre)
-        (fun th -> pool_alive #e p ** joinable th)
-
-(* Spawn of a unit-returning task with no intention to join, simpler. *)
-val spawn_
-  (#pre #post : _)
-  (p:pool)
-  (#[T.exact (`1.0R)] e : perm)
+val pool_alive (#[T.exact (`1.0R)] f : perm) (p:pool) : slprop
+
+val joinable (p: pool) (post: slprop) (h: handle) : slprop
+
+fn spawn
+  (p: pool)
+  (#pf: perm)
+  (#pre: slprop)
+  (#post: slprop)
   (f : unit -> stt unit pre (fun _ -> post))
-  : stt unit (pool_alive #e p ** pre)
-             (fun prom -> pool_alive #e p ** pledge emp_inames (pool_done p) post)
+  requires pool_alive #pf p ** pre
+  returns h : handle
+  ensures pool_alive #pf p ** joinable p post h
 
-(* If the pool is done, all pending joinable threads must be done *)
-val must_be_done
+val pool_done (p:pool) : slprop
+
+ghost
+fn disown
   (#p : pool)
-  (#a: Type0)
-  (#post : a -> slprop)
-  (th : task_handle p a post)
-  : stt_ghost unit emp_inames (pool_done p ** joinable th) (fun () -> pool_done p ** handle_solved th)
-
-val join0
-  (#p:pool)
-  (#a:Type0)
-  (#post : a -> slprop)
-  (th : task_handle p a post)
-  : stt unit (joinable th) (fun () -> handle_solved th)
-
-val extract
-  (#p:pool)
-  (#a:Type0)
-  (#post : a -> slprop)
-  (th : task_handle p a post)
-  : stt a (handle_solved th) (fun x -> post x)
-
-val share_alive
+  (#post : slprop)
+  (h : handle)
+  requires joinable p post h
+  ensures  pledge [] (pool_done p) post
+
+(* spawn + disown *)
+fn spawn_
+  (p: pool)
+  (#pf : perm)
+  (#pre : slprop)
+  (#post : slprop)
+  (f : unit -> stt unit (pre) (fun _ -> post))
+  requires pool_alive #pf p ** pre
+  ensures pool_alive #pf p ** pledge [] (pool_done p) post
+
+fn await
+  (#p: pool)
+  (#post : slprop)
+  (h : handle)
+  (#f : perm)
+  requires pool_alive #f p ** joinable p post h
+  ensures pool_alive #f p ** post
+
+fn await_pool
   (p:pool)
-  (e:perm)
-  : stt_ghost unit
-              emp_inames
-              (pool_alive #e p)
-              (fun () -> pool_alive #(e /. 2.0R) p ** pool_alive #(e /. 2.0R) p)
+  (#is:inames)
+  (#f:perm)
+  (q : slprop)
+  requires pool_alive #f p ** pledge is (pool_done p) q
+  ensures pool_alive #f p ** q
 
-val gather_alive
+fn teardown_pool
   (p:pool)
-  (e:perm)
-  : stt_ghost unit
-              emp_inames
-              (pool_alive #(e /. 2.0R) p ** pool_alive #(e /. 2.0R) p)
-              (fun () -> pool_alive #e p)
-
-val join
-  (#p:pool)
-  (#a:Type0)
-  (#post : a -> slprop)
-  (th : task_handle p a post)
-  : stt a (joinable th) (fun x -> post x)
-
-(* We must exclusively own the pool in order to terminate it. *)
-val teardown_pool
+  requires pool_alive p
+  ensures pool_done p
+
+ghost
+fn share_alive
   (p:pool)
-  : stt unit (pool_alive #1.0R p) (fun _ -> pool_done p)
+  (e:perm)
+  requires pool_alive #e p
+  ensures pool_alive #(e /. 2.0R) p ** pool_alive #(e /. 2.0R) 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:inames)
-  (p:pool) (f:perm{f <. 1.0R})
-  : stt unit (pool_alive #f p ** pledge is (pool_done p) (pool_alive #(1.0R -. f) p))
-             (fun _ -> pool_done p)
+ghost
+fn gather_alive
+  (p:pool)
+  (e:perm)
+  requires pool_alive #(e /. 2.0R) p ** pool_alive #(e /. 2.0R) p
+  ensures pool_alive #e p
+
+fn setup_pool
+  (n: pos)
+  requires emp
+  returns p : pool
+  ensures pool_alive p

qs/Makefile

@@ -5,15 +5,19 @@ OTHERFLAGS += --ext pulse:extract_ocaml_bare
 DEPFLAGS += --extract '-*'
 DEPFLAGS += --extract +Quicksort
 DEPFLAGS += --extract +Pulse.Lib.Dv
-# DEPFLAGS += --extract +NuPool
+# DEPFLAGS += --extract +Pulse.Lib.Task
 # DEPFLAGS += --extract +Pulse.Class.Duplicable
 # DEPFLAGS += --extract +FStar.Dyn # wrong. it's int FStarC_Dyn.ml
 
 include fstar.mk
-all: _output/Quicksort_Task.exe
 
-_output/Quicksort_Task.exe: $(ALL_ML_FILES)
-	eval $$(OPAMSWITCH=5.1.1 opam env) && /home/guido/.opam/5.1.1/bin/dune build --root=dune
+.PHONY: all
+all: run
 
-run:
+.PHONY: dune
+dune: $(ALL_ML_FILES)
+	opam exec --switch=5.1.1 -- dune build --root=dune
+
+.PHONY: run
+run: dune
 	./dune/_build/default/driver.exe

qs/README.md

@@ -0,0 +1,9 @@
+# Parallel quicksort extracted to OCaml 5
+
+This directory contains the build infrastructure to extract the Quicksort.Task file to OCaml, and build it with OCaml 5.1.1 and domainslib.
+
+```shell
+opam switch create 5.1.1
+opam install --switch=5.1.1 domainslib
+make
+```

qs/fstar.mk

@@ -20,7 +20,7 @@ include common.mk
 .DEFAULT_GOAL := all
 
 # Set a default FSTAR_EXE for most clients.
-FSTAR_EXE ?= $(FSTAR_ROOT)/bin/fstar.exe
+FSTAR_EXE ?= $(FSTAR_HOME)/bin/fstar.exe
 FSTAR_EXE := $(abspath $(FSTAR_EXE))
 export FSTAR_EXE
 

share/pulse/examples/MSort.Task.fst

@@ -22,7 +22,7 @@ module S = FStar.Seq
 module SZ = FStar.SizeT
 open MSort.SeqLemmas
 open MSort.Base
-open NuPool
+open Pulse.Lib.Task
 
 
 fn rec t_msort_par

share/pulse/examples/Quicksort.Task.fst

@@ -23,7 +23,7 @@ module R = Pulse.Lib.Reference
 module SZ = FStar.SizeT
 module GSet = FStar.GhostSet
 
-module T = NuPool
+module T = Pulse.Lib.Task
 open Quicksort.Base
 open Pulse.Lib.Pledge
 

share/pulse/examples/parix/ParallelFor.fst

@@ -19,7 +19,7 @@ module ParallelFor
 
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Fixpoints
-open NuPool
+open Pulse.Lib.Task
 open FStar.Real
 open Pulse.Lib.Pledge
 open Pulse.Lib.OnRange

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

@@ -19,7 +19,7 @@ module TaskPool.Examples
 
 open Pulse.Lib.Pervasives
 open Pulse.Lib.Pledge
-open NuPool
+open Pulse.Lib.Task
 
 assume
 val qsv : nat -> slprop