Add lockdown semantics to CanonicalABI.md

design/mvp/CanonicalABI.md

@@ -89,10 +89,22 @@ boilerplate. For a complete listing of all Python definitions in a single
 executable file with a small unit test suite, see the
 [`canonical-abi`](canonical-abi/) directory.
 
-The convention followed by the Python code below is that all traps are raised
-by explicit `trap()`/`trap_if()` calls; Python `assert()` statements should
-never fire and are only included as hints to the reader. Similarly, there
-should be no uncaught Python exceptions.
+The convention followed by the Python code below is that all traps are raised by
+explicit `trap()`/`trap_if()` calls. Python `assert()` statements should never
+fire; their conditions are maintained either by the internal rules of the
+Component Model or by the host following the rules of the Embedding API.
+
+As required by [Component Invariant] #1, any trap must lock down the entire
+containing store as defined in the `Store` class below:
+```python
+def trap():
+  current_instance().store.lock_down()
+  raise Trap()
+
+def trap_if(cond):
+  if cond:
+    trap()
+```
 
 While the Python code for lifting and lowering values appears to create an
 intermediate copy when lifting linear memory into high-level Python values, a
@@ -845,26 +857,42 @@ in chunks, the `Store` constructor is analogous to Core WebAssembly
 class Store:
   waiting: list[Thread]
   nesting_depth: int
+  lockdown: bool
 
   def __init__(self):
     self.waiting = []
     self.nesting_depth = 0
+    self.lockdown = False
 ```
 The `waiting` field is populated by `Thread` methods, as defined above, and the
 `nesting_depth` field is purely a specification device used by `Store` methods
 below to define the valid host call interleavings (and, in particular, when it
 is valid to call `Store.tick`).
 
+The `Store.lockdown` flag is used to specify [Component Invariant] #1. This flag
+can be queried and set directly by the host through the Embedding API:
+```python
+  def is_locked_down(self):
+    return self.lockdown
+
+  def lock_down(self):
+    self.lockdown = True
+```
+
 The `Store.invoke` method is analogous to Core WebAssembly's [`func_invoke`] and
 takes a `FuncInst` (analogous to a Core WebAssembly [`funcinst`]) along with its
 runtime `OnStart` and `OnResolve` arguments (which are described above alongside
-their definitions).
+their definitions). The `not lockdown` assertions require the host not to start
+any new calls or cancel any existing calls (which may execute guest code) once
+the store has been locked down.
 ```python
   def invoke(self, f: FuncInst, on_start: OnStart, on_resolve: OnResolve) -> OnCancel:
+    assert(not self.lockdown)
     self.nesting_depth += 1
     request_cancellation = f(on_start, on_resolve)
     self.nesting_depth -= 1
     def on_cancel():
+      assert(not self.lockdown)
       self.nesting_depth += 1
       request_cancellation()
       self.nesting_depth -= 1
@@ -919,6 +947,7 @@ progress and the expectation is that the host heuristically interleaves calls to
 while new tasks are being started.
 ```python
   def tick(self):
+    assert(not self.lockdown)
     assert(self.nesting_depth == 0)
     self.nesting_depth += 1
     candidates = { thread for thread in self.waiting if thread.ready() }
@@ -927,10 +956,12 @@ while new tasks are being started.
       thread.resume()
     self.nesting_depth -= 1
 ```
-As shown above, `Store.nesting_depth` is greater than zero while calling
-`Store.invoke` or cancelling via the `OnCancel` callback and thus the `assert`
-prohibits the host from scheduling arbitrary store-wide cooperative threads
-until all core wasm calls on the stack have [blocked] or returned.
+The `not lockdown` assertion complements those in `Store.invoke` and prohibits
+the host from resuming concurrent tasks in a locked-down store. Since
+`Store.nesting_depth` is greater than zero while calling `Store.invoke` or
+`on_cancel`, the `nesting_depth == 0` assertion further prohibits the host from
+scheduling arbitrary cooperative threads until all active core wasm calls in the
+store have [blocked] or returned.
 
 
 ## Canonical ABI Options

design/mvp/Explainer.md

@@ -3088,10 +3088,9 @@ In particular, the Component Model maintains the following invariants:
    also allows more-aggressive compiler optimizations (e.g., store reordering).
    This was considered early in Core WebAssembly standardization but rejected
    due to the lack of clear trapping boundary. With components, each component
-   instance is given a mutable "lockdown" state that is set upon trap and
-   implicitly checked at every execution step by component functions. Thus,
-   after a trap, it's no longer possible to observe the internal state of a
-   component instance.
+   store is given a mutable "lockdown" state that is set upon trap and checked
+   at all reentry points. Thus, after a trap, it's no longer possible to observe
+   the internal state of a component instance.
 
 2. When components implement `async` functions using the 0.3.0 sync or
    async-callback ABIs, core wasm execution is "run to completion" within the

design/mvp/canonical-abi/definitions.py

@@ -15,13 +15,6 @@
 class Trap(BaseException): pass
 class CoreWebAssemblyException(BaseException): pass
 
-def trap():
-  raise Trap()
-
-def trap_if(cond):
-  if cond:
-    raise Trap()
-
 class Type: pass
 class ValType(Type): pass
 class ExternType(Type): pass
@@ -184,6 +177,14 @@ class FutureType(ValType):
 
 # START
 
+def trap():
+  current_instance().store.lock_down()
+  raise Trap()
+
+def trap_if(cond):
+  if cond:
+    trap()
+
 ## Component Instances
 
 class ComponentInstance:
@@ -511,16 +512,26 @@ def cancel(self):
 class Store:
   waiting: list[Thread]
   nesting_depth: int
+  lockdown: bool
 
   def __init__(self):
     self.waiting = []
     self.nesting_depth = 0
+    self.lockdown = False
+
+  def is_locked_down(self):
+    return self.lockdown
+
+  def lock_down(self):
+    self.lockdown = True
 
   def invoke(self, f: FuncInst, on_start: OnStart, on_resolve: OnResolve) -> OnCancel:
+    assert(not self.lockdown)
     self.nesting_depth += 1
     request_cancellation = f(on_start, on_resolve)
     self.nesting_depth -= 1
     def on_cancel():
+      assert(not self.lockdown)
       self.nesting_depth += 1
       request_cancellation()
       self.nesting_depth -= 1
@@ -546,6 +557,7 @@ def core_func_inst(args: list[CoreValType]) -> list[CoreValType]:
     return core_func_inst
 
   def tick(self):
+    assert(not self.lockdown)
     assert(self.nesting_depth == 0)
     self.nesting_depth += 1
     candidates = { thread for thread in self.waiting if thread.ready() }

design/mvp/canonical-abi/run_tests.py

@@ -104,6 +104,16 @@ def unpack_new_ends(packed):
 def fail(msg):
   raise BaseException(msg)
 
+def expect_fail(f, msg = "expected a trap"):
+  store = current_instance().store
+  try:
+    f()
+  except Trap:
+    assert(store.is_locked_down())
+    store.lockdown = False
+    return
+  fail(msg)
+
 def test(t, vals_to_lift, v,
          cx = mk_cx(),
          dst_encoding = None,
@@ -112,35 +122,46 @@ def test(t, vals_to_lift, v,
   def test_name():
     return "test({},{},{}):".format(t, vals_to_lift, v)
 
-  vi = CoreValueIter(vals_to_lift)
-
-  if v is None:
+  error = None
+  def thread_func():
+    nonlocal error, cx, dst_encoding, lower_t, lower_v
     try:
-      got = lift_flat(cx, vi, t)
-      fail("{} expected trap, but got {}".format(test_name(), got))
-    except Trap:
-      return
-
-  got = lift_flat(cx, vi, t)
-  assert(vi.i == len(vi.values))
-  if got != v:
-    fail("{} initial lift_flat() expected {} but got {}".format(test_name(), v, got))
-
-  if lower_t is None:
-    lower_t = t
-  if lower_v is None:
-    lower_v = v
+      vi = CoreValueIter(vals_to_lift)
 
-  heap = Heap(5*len(cx.opts.memory))
-  if dst_encoding is None:
-    dst_encoding = cx.opts.string_encoding
-  cx = mk_cx(MemInst(heap.memory, cx.opts.memory.ptr_type()), dst_encoding, heap.realloc)
-  lowered_vals = lower_flat(cx, v, lower_t)
+      if v is None:
+        def lift_expecting_trap():
+          got = lift_flat(cx, vi, t)
+          fail("{} expected trap, but got {}".format(test_name(), got))
+        expect_fail(lift_expecting_trap)
+        return
 
-  vi = CoreValueIter(lowered_vals)
-  got = lift_flat(cx, vi, lower_t)
-  if not equal_modulo_string_encoding(got, lower_v):
-    fail("{} re-lift expected {} but got {}".format(test_name(), lower_v, got))
+      got = lift_flat(cx, vi, t)
+      assert(vi.i == len(vi.values))
+      if got != v:
+        fail("{} initial lift_flat() expected {} but got {}".format(test_name(), v, got))
+
+      if lower_t is None:
+        lower_t = t
+      if lower_v is None:
+        lower_v = v
+
+      heap = Heap(5*len(cx.opts.memory))
+      if dst_encoding is None:
+        dst_encoding = cx.opts.string_encoding
+      cx = mk_cx(MemInst(heap.memory, cx.opts.memory.ptr_type()), dst_encoding, heap.realloc)
+      lowered_vals = lower_flat(cx, v, lower_t)
+
+      vi = CoreValueIter(lowered_vals)
+      got = lift_flat(cx, vi, lower_t)
+      if not equal_modulo_string_encoding(got, lower_v):
+        fail("{} re-lift expected {} but got {}".format(test_name(), lower_v, got))
+    except BaseException as e:
+      error = e
+
+  task = Task(FuncType([],[]), CanonicalOptions(), cx.inst, lambda: [], lambda _: ())
+  Thread(task, thread_func).resume()
+  if error is not None:
+    raise error
 
 # Empty record types are not permitted yet.
 #test(RecordType([]), [], {})
@@ -477,11 +498,13 @@ def test_trap_propagation():
   def core_func(args):
     trap()
 
+  assert(not store.is_locked_down())
   try:
     lift_and_run(mk_opts(), inst, FuncType([], []), core_func, lambda:[], lambda _:())
     fail("expected the guest trap to propagate out of Store.invoke")
   except Trap:
     pass
+  assert(store.is_locked_down())
 
 
 def test_cross_component_realloc():
@@ -521,11 +544,7 @@ def core_consumer_realloc(args):
     assert(canon_context_get('i32', 1) == [0])
     [] = canon_context_set('i32', 0, 0xfeed)
     assert(canon_context_get('i32', 0) == [0xfeed])
-    try:
-      canon_thread_index()
-      fail("thread.index must trap during realloc")
-    except Trap:
-      pass
+    expect_fail(canon_thread_index, "thread.index must trap during realloc")
     return consumer_heap.realloc(args)
 
   consumer_opts = mk_opts(MemInst(consumer_heap.memory, 'i32'), realloc = core_consumer_realloc)
@@ -2319,12 +2338,7 @@ def core_func(args):
 
     [packed] = canon_future_new(FutureType(U8Type()))
     rfi,wfi = unpack_new_ends(packed)
-    trapped = False
-    try:
-      canon_future_drop_writable(FutureType(U8Type()), wfi)
-    except Trap:
-      trapped = True
-    assert(trapped)
+    expect_fail(lambda: canon_future_drop_writable(FutureType(U8Type()), wfi))
 
     return []
 
@@ -2400,12 +2414,7 @@ def core_func(args):
     assert(n == 0 and result == CopyResult.DROPPED)
     [event] = canon_waitable_set_poll(MemInst(mem, 'i32'), seti, retp)
     assert(event == EventCode.NONE)
-    trapped = False
-    try:
-      canon_stream_read(stream_t, opts, rsi, 0, 4)
-    except Trap:
-      trapped = True
-    assert(trapped)
+    expect_fail(lambda: canon_stream_read(stream_t, opts, rsi, 0, 4))
     [] = canon_waitable_join(rsi, 0)
     [] = canon_stream_drop_readable(stream_t, rsi)
 
@@ -2523,11 +2532,7 @@ def core_sync_import(args):
     [x] = args
     [result] = store.lower(host_func1_inst, ft, sync_lower_opts, callee_inst)([42])
     assert(result == 43)
-    try:
-      [] = canon_task_cancel()
-      assert(False)
-    except Trap:
-      pass
+    expect_fail(canon_task_cancel)
     [si] = canon_waitable_set_new()
     [] = canon_context_set('i32', 0, si)
     return [CallbackCode.WAIT | (si << 4)]