Extracting Quicksort.Task

qs/.gitignore

@@ -0,0 +1,2 @@
+_cache
+_output

qs/Makefile

@@ -0,0 +1,19 @@
+OTHERFLAGS += --include ../lib
+OTHERFLAGS += --include ../share/pulse/examples
+OTHERFLAGS += --ext pulse:extract_ocaml_bare
+
+DEPFLAGS += --extract '-*'
+DEPFLAGS += --extract +Quicksort
+DEPFLAGS += --extract +Pulse.Lib.Dv
+# DEPFLAGS += --extract +NuPool
+# 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
+
+run:
+	./dune/_build/default/driver.exe

qs/NuPool.ml

@@ -0,0 +1,64 @@
+(* This is a quick-and-dirty wrapper over Domainslib.Task
+   that makes teardown_pool wait until all tasks have finished,
+   instead of being unspecified in that case. *)
+
+module T = Domainslib.Task
+module A = Atomic
+module S = Semaphore.Binary
+open Either
+
+let dbg s = () (* print_string (s ^ "\n"); flush stdout *)
+
+type 'a task = 'a T.task
+
+type !'a promise = 'a T.promise
+
+type pool = {
+    p   : T.pool;
+    ctr : int Atomic.t;
+    sem : S.t;
+}
+
+let setup_pool num_domains =
+    let p = T.setup_pool ~num_domains () in
+    let ctr = Atomic.make 0 in
+    let sem = S.make false in
+    { p; ctr; sem }
+
+let teardown_pool p =
+    (* S.acquire p.sem; *)
+    T.teardown_pool p.p
+
+let wrap_task p (t : 'a task) : 'a task = fun () ->
+    let r =
+        match t () with
+        | exception ex -> Left ex
+        | v -> Right v
+    in
+    let c = A.fetch_and_add p.ctr (-1) in
+    if c = 1 then (* c == old value *)
+        S.release p.sem;
+    match r with
+    | Left ex -> raise ex (* this will mess with stack traces, but at least won't deadlock *)
+    | Right v -> v
+
+let run p t =
+    ignore (A.fetch_and_add p.ctr 1);
+    T.run p.p (wrap_task p t)
+
+let async p t =
+    ignore (A.fetch_and_add p.ctr 1);
+    T.async p.p (wrap_task p t)
+
+let await p h =
+    T.await p.p h
+
+let await_pool p () () () =
+    dbg "await_pool.1";
+    S.acquire p.sem (* not right *) ;
+    dbg "await_pool.2";
+    ()
+
+let spawn_ p () () () f =
+    let _ = async p f in
+    ()

qs/Quicksort.Task.fst

@@ -0,0 +1 @@
+../share/pulse/examples/Quicksort.Task.fst

qs/common.mk

@@ -0,0 +1,92 @@
+# This makefile is included from several other makefiles in the tree.
+
+MAKEFLAGS += --no-builtin-rules
+Q?=@
+SIL?=--silent
+RUNLIM=
+ifneq ($(V),)
+	Q=
+	SIL=
+else
+	MAKEFLAGS += -s
+endif
+
+define NO_RUNLIM_ERR
+runlim not found:
+  To use RESOURCEMONITOR=1, the `runlim` tool must be installed and in your $$PATH.
+  It must also be a recent version supporting the `-p` option.
+  You can get it from: [https://github.com/arminbiere/runlim]
+endef
+
+define msg =
+@printf "   %-14s  %s\n" $(1) $(2)
+endef
+define bold_msg =
+@#-tput bold 2>/dev/null
+@printf -- "  %-15s" $(1)
+@#-tput sgr0 2>/dev/null
+@printf "  %s\n" $(2)
+endef
+
+# Passing RESOURCEMONITOR=1 will create .runlim files through the source tree with
+# information about the time and space taken by each F* invocation.
+ifneq ($(RESOURCEMONITOR),)
+	ifeq ($(shell which runlim),)
+		_ := $(error $(NO_RUNLIM_ERR)))
+	endif
+	ifneq ($(MONID),)
+		MONPREFIX=$(MONID).
+	endif
+	RUNLIM=runlim -p -o $@.$(MONPREFIX)runlim
+endif
+
+# Ensure that any failing rule will not create its target file.
+# In other words, make `make` less insane.
+.DELETE_ON_ERROR:
+
+.DEFAULT_GOAL:=__undef
+.PHONY: __undef
+__undef:
+	$(error "This makefile does not have a default goal")
+
+# Check that a variable is defined. If not, abort with an (optional) error message.
+need =												\
+  $(if $(value $(strip $1)),,									\
+    $(error Need a value for $(strip $1)$(if $2, ("$(strip $2)"))))
+
+# Check that a variable is defined and pointing to an executable.
+# Is there no negation in make...?
+# Wew! this was interesting to write. Especially the override part.
+need_exe =											\
+  $(if $(value $(strip $1)),									\
+    $(if $(wildcard $(value $(strip $1))),							\
+      $(if $(shell test -x $(value $(strip $1)) && echo 1),					\
+        $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
+        $(error $(strip $1) ("$(value $(strip $1))") is not executable)),			\
+      $(error $(strip $1) ("$(value $(strip $1))") does not exist (cwd = $(CURDIR)))),		\
+    $(error Need an executable for $(strip $1)$(if $2, ("$(strip $2)"))))			\
+
+need_file =											\
+  $(if $(value $(strip $1)),									\
+    $(if $(wildcard $(value $(strip $1))),							\
+      $(if $(shell test -f $(value $(strip $1)) && echo 1),					\
+        $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
+        $(error $(strip $1) ("$(value $(strip $1))") is not executable)),			\
+      $(error $(strip $1) ("$(value $(strip $1))") does not exist (cwd = $(CURDIR)))),		\
+    $(error Need a file path for $(strip $1)$(if $2, ("$(strip $2)"))))				\
+
+need_dir =											\
+  $(if $(value $(strip $1)),									\
+    $(if $(wildcard $(value $(strip $1))),							\
+      $(if $(shell test -d $(value $(strip $1)) && echo 1),					\
+        $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
+        $(error $(strip $1) ("$(value $(strip $1))") is not executable)),			\
+      $(error $(strip $1) ("$(value $(strip $1))") is not a directory (cwd = $(CURDIR)))),	\
+    $(error Need an *existing* directory path for $(strip $1)$(if $2, ("$(strip $2)"))))	\
+
+need_dir_mk =											\
+  $(if $(value $(strip $1)),									\
+    $(if $(shell mkdir -p $(value $(strip $1)) && echo 1),					\
+      $(eval override $(strip $1):=$(abspath $(value $(strip $1)))),				\
+      $(error $(strip $1) ("$(value $(strip $1))") is not a directory (mkdir failed, cwd = $(CURDIR)))),	\
+    $(error Need a directory path for $(strip $1)$(if $2, ("$(strip $2)"))))			\

qs/driver.ml

@@ -0,0 +1,22 @@
+let dbg s = print_string (s ^ "\n"); flush stdout
+
+let main =
+  let nproc = 32 in
+  let len = 100000000 in
+  let a = Array.make len 0 in
+  for i = 0 to len - 1 do
+    a.(i) <- Random.int 100000000
+  done;
+  (* print_string "BEFORE: "; *)
+  (* Array.iter (fun x -> print_int x; print_string " ") a; *)
+  (* print_newline (); *)
+  (* dbg "calling quicksort"; *)
+  Quicksort_Task.quicksort nproc a 0 len () () ();
+  (* print_string "AFTER: "; *)
+  (* Array.iter (fun x -> print_int x; print_string " ") a; *)
+  (* print_newline (); *)
+  (* check that it's sorted... *)
+  let old = ref 0 in
+  Array.iter (fun x -> if x < !old then failwith "not sorted"; old := x) a;
+  print_string "ok!\n";
+  ()

qs/dune/.gitignore

@@ -0,0 +1 @@
+_build

qs/dune/NuPool.ml

@@ -0,0 +1 @@
+../NuPool.ml

qs/dune/Prims.ml

@@ -0,0 +1,12 @@
+(* cannot redefine bool=bool, it's cyclic *)
+type bool' = bool
+type bool = bool'
+type int' = int
+type int = int'
+
+let of_int x = x 
+let int_zero = 0
+let int_one = 1
+
+type nat = int
+type pos = int

qs/dune/driver.ml

@@ -0,0 +1 @@
+../driver.ml

qs/dune/dune

@@ -0,0 +1,10 @@
+(include_subdirs unqualified)
+(executable
+ (name driver)
+ (public_name qsort.exe)
+ (libraries domainslib)
+ (modes native byte)
+)
+(env
+  (_
+    (flags (:standard -w -A))))

qs/dune/dune-project

@@ -0,0 +1,7 @@
+(lang dune 3.8)
+(name qsort)
+
+(package
+  (name qsort)
+  (synopsis "An example F* application")
+)

qs/dune/output

@@ -0,0 +1 @@
+../_output/