From 148c7598fdd52d9d0faa09de897a93ee64404733 Mon Sep 17 00:00:00 2001 From: Dan Gooding Date: Tue, 3 May 2022 21:46:50 +0100 Subject: [PATCH 1/3] Add test of `under`'s masking when perform `fun` in-place --- compile.sh | 2 +- test/semantics/under-mask.t/run.t | 9 +++++++++ test/semantics/under-mask.t/under.kk | 28 ++++++++++++++++++++++++++++ 3 files changed, 38 insertions(+), 1 deletion(-) create mode 100644 test/semantics/under-mask.t/run.t create mode 100644 test/semantics/under-mask.t/under.kk diff --git a/compile.sh b/compile.sh index 67549df..f31c241 100755 --- a/compile.sh +++ b/compile.sh @@ -17,7 +17,7 @@ else fi # intentionally rely on clang to know the system's target triple -LL_C_FLAGS="-Wall -Wno-override-module -O$OPT_LEVEL" +LL_C_FLAGS="-Wall -Wno-override-module -O$OPT_LEVEL" # -fno-optimize-sibling-calls RUNTIME=$PROJECT_ROOT/lib/runtime/runtime.c diff --git a/test/semantics/under-mask.t/run.t b/test/semantics/under-mask.t/run.t new file mode 100644 index 0000000..7534b5b --- /dev/null +++ b/test/semantics/under-mask.t/run.t @@ -0,0 +1,9 @@ +`fun` opertions may be run at the perform-site, but they should +appear to run at the handler-site + $ koka-zero interpret under.kk + 1 + + $ export PROJECT_ROOT=../../.. + $ ../compile.sh under.kk + $ ./under + 1 diff --git a/test/semantics/under-mask.t/under.kk b/test/semantics/under-mask.t/under.kk new file mode 100644 index 0000000..359f729 --- /dev/null +++ b/test/semantics/under-mask.t/under.kk @@ -0,0 +1,28 @@ +effect ask { + fun ask(x : ()) : int; +}; + +effect fail { + control fail(x : ()) : (); +}; + +fun main() { + with handler { + control fail(_) { // fail must be handled here + print-int(1) + }; + }; + with handler { + fun ask(_) { // runs in-place at the perform-site of ask(()) + fail(()); -1; + }; + }; + with handler { + control fail(_) { // fail must not be handled here + print-int(0); + }; + }; + // perform ask(()) + ask(()); + (); +}; From a862eea48d915269662539a26dc46a5209a3bea4 Mon Sep 17 00:00:00 2001 From: Dan Gooding Date: Tue, 3 May 2022 22:38:30 +0100 Subject: [PATCH 2/3] Add test which fails to typecheck due occurs check Perhaps can skip inference phase? Or else wrap resume into a datatype to hide the recursion --- test/semantics/underk-refinding.t/run.t | 17 ++++++++ test/semantics/underk-refinding.t/underk.kk | 45 +++++++++++++++++++++ 2 files changed, 62 insertions(+) create mode 100644 test/semantics/underk-refinding.t/run.t create mode 100644 test/semantics/underk-refinding.t/underk.kk diff --git a/test/semantics/underk-refinding.t/run.t b/test/semantics/underk-refinding.t/run.t new file mode 100644 index 0000000..92f994f --- /dev/null +++ b/test/semantics/underk-refinding.t/run.t @@ -0,0 +1,17 @@ +Fixing the handler-site vector `w_handler` in `under` neglects +the possiblity of the handler itself being suspended and resumed +somewhere else. + +Taken from Section 2.9.2 of "Generalized Evidence Passing for Effect Handlers +(or, Efficient Compilation of Effect Handlers to C)" +by Ningning Xie and Daan Leijen + + $ koka-zero interpret underk.kk + 1 + 2 + + $ export PROJECT_ROOT=../../.. + $ ../compile.sh underk.kk + $ ./underk + 1 + 2 diff --git a/test/semantics/underk-refinding.t/underk.kk b/test/semantics/underk-refinding.t/underk.kk new file mode 100644 index 0000000..583c917 --- /dev/null +++ b/test/semantics/underk-refinding.t/underk.kk @@ -0,0 +1,45 @@ +effect evil { + control evil(x : ()) : (); +}; + +// not relevant that `read` is tail-resumptive +effect read { + fun ask(x : ()) : int; +}; + +// relevant that `tl` is tail resumptive! +effect tl { + fun tl(x : ()) : int; +}; + +// run a resumption under a different handler context +fun f(k) { + with handler { // h_read2 + fun ask(_) { 2 }; + }; + k(()); // 5: resume `evil` now with a different `ask` handler +}; + +fun g() { + with handler { // h_read1 + fun ask(_) { 1 }; + }; + with handler { // h_evil + control evil(_) { + // 4: leak resumption to later resume under changed handler context + resume; // FIXME: leaking like this fails the occurs check :/ + }; + }; + with handler { // h_tl + fun tl(_) { + ask(()).print-int(); // 2: receive value 1 + evil(()); // 3: perform `evil` within tail-resumptive operation clause + ask(()).print-int(); // 6: recieve value 2 + }; + }; + tl(); // 1: perform `tl` +}; + +fun main() { + f(g()); +}; From 4b7d0eee0a722975bcf61e29baa57eea8743fedd Mon Sep 17 00:00:00 2001 From: Dan Gooding Date: Tue, 3 May 2022 22:42:04 +0100 Subject: [PATCH 3/3] Revert comment added to compile.sh --- compile.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compile.sh b/compile.sh index f31c241..67549df 100755 --- a/compile.sh +++ b/compile.sh @@ -17,7 +17,7 @@ else fi # intentionally rely on clang to know the system's target triple -LL_C_FLAGS="-Wall -Wno-override-module -O$OPT_LEVEL" # -fno-optimize-sibling-calls +LL_C_FLAGS="-Wall -Wno-override-module -O$OPT_LEVEL" RUNTIME=$PROJECT_ROOT/lib/runtime/runtime.c