diff --git a/test/programs/pool-stale-region.flan b/test/programs/pool-stale-region.flan new file mode 100644 index 0000000..028e92c --- /dev/null +++ b/test/programs/pool-stale-region.flan @@ -0,0 +1,25 @@ +;;;; The epoch trap on the pool's side. spec-memory.md, "Dev builds detect a +;;;; released region". +;;;; +;;;; This is deliberately the *other* failure from a stale handle, and the two +;;;; must not be conflated — the same rule that keeps a Vec's generation word +;;;; and its epoch word apart. A stale handle is an answer: the entity died, +;;;; resolve says None, the program carries on. A released region is not an +;;;; answer at all: the storage the pool sits in is gone, the slot array with +;;;; it, and there is nothing left to ask. So one returns None and the other +;;;; traps naming the site. +(defn main [] i32 + (let [a (arena-new 4096)] + (let [p (pool-new i32 a)] + (let [h (insert p 7)] + (match (resolve p h) + (Some x) (println (deref x)) + None (println -1)) + ;; The region goes. p is still in scope, still looks fine, and h is + ;; still a perfectly well-formed handle — which is exactly the case a + ;; static rule cannot see. + (free-all a) + (match (resolve p h) + (Some x) (println (deref x)) + None (println -1))))) + 0) diff --git a/test/test_acceptance.ml b/test/test_acceptance.ml index 54fd10b..15d2ead 100644 --- a/test/test_acceptance.ml +++ b/test/test_acceptance.ml @@ -691,6 +691,41 @@ let () = end; (try Sys.remove exe with Sys_error _ -> ()); + (* (Handle T) and (Pool T), spec-memory.md. The thesis is one line of this + output and the rest is scaffolding for it: the same slot prints as + before a death and after the reuse, and the + projectile still holding the first is told -1 rather than the + newcomer's 99. At -O0 as well, because the null test resolve is built + out of is exactly the kind of control flow an optimiser launders, and + as a dev build, because a pool then lives in a frame the reload path + has to agree with on 64 bytes. *) + let handles_out = + "3\n3\n60\n21\ntrue\nfalse\n2\n\n\nfalse\ntrue\n-1\n99\n3\n3\n\n-1\n10\n30\n" + in + outputs "handles" "programs/handles.flan" handles_out; + outputs ~opt:"-O0" "handles, -O0" "programs/handles.flan" handles_out; + outputs ~dev:true "handles, dev" "programs/handles.flan" handles_out; + + (* The epoch trap on the pool's side, and it is deliberately the *other* + failure from a stale handle. A stale handle is an answer and resolve + returns None; a released region is not an answer at all, because the + slot array went with the storage, so it traps. The two must not be + conflated, which is the same rule that keeps a Vec's generation word + and its epoch word apart. *) + let exe = compile "programs/pool-stale-region.flan" in + let code, text = run exe None in + if code <> 134 || not (contains text "programs/pool-stale-region.flan:") + || not (contains text "allocator was released") + || not (contains text "7") + then begin + incr failures; + Printf.printf + "FAIL a pool used after its region was released\n\ + \ got: %S (exit %d)\n wanted: exit 134, naming the site\n" + text code + end; + (try Sys.remove exe with Sys_error _ -> ()); + (* The same trap on the Map's side, and it is not the same code path: a Vec's operations check on the way in and stop there, while a map's get goes on to call a hash and an equality function through pointers into diff --git a/test/test_flan.ml b/test/test_flan.ml index bca099d..d040cea 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -835,6 +835,33 @@ let () = ~needle:"exactly two types"; rejects_check "Result is milestone 6" "(defn f [] (Result i32 i32) None)" ~needle:"milestone 6"; + (* (Handle T) and (Pool T) are built. What stays refused is the arity, for + the reason Vec's and Map's arities are, and the four shapes below — each + of which is a way of losing the one property the type exists to have. *) + rejects_check "Handle takes one type" "(defn f [x (Handle i32 i32)] ())" + ~needle:"exactly one type"; + rejects_check "Pool takes one type" "(defn f [x (Pool i32 i32)] ())" + ~needle:"exactly one type"; + (* A pool of an owning element, refused where a Vec of a Vec is refused and + for the same reason: the runtime copies and releases slots bytewise. *) + rejects_check "a pool of a Vec" + "(defn f [x (Pool (Vec i32))] ())" ~needle:"move-only element"; + (* Ordering handles would order a slot index, which is a free-list artefact. + Equality is admitted and ordering is not, which is why there are two + predicates in Types rather than one. *) + rejects_check "handles do not order" + "(defn f [a (Handle i32) b (Handle i32)] bool (< a b))" + ~needle:"no built-in comparison"; + (* free takes the owner. A handle is a copyable number that owns nothing, so + consuming one copy would say nothing about the others — which is why a + slot is recycled by (release p h) and not by free. *) + rejects_check "free of a handle" + "(defn f [h (Handle i32)] () (free h))" ~needle:"a handle owns nothing"; + (* Cloning a pool would duplicate the generation counters with the slots, so + one handle would resolve in both copies and name two different things. *) + rejects_check "a pool cannot be cloned" + "(defn f [p (Pool i32)] () (let [q (clone p)] (do)))" + ~needle:"cannot be cloned"; rejects_check "try is milestone 6" "(defn f [] i32 (try 1))" ~needle:"milestone 6"; (* dotimes and defer are implemented, and a defer in a [let] is now one of