According to the specification section 9.1.9:
THR: AWAIT(THR: thread) = MUST block until thread has finished and then return the same thread handle.
THR: PAUSE(THR: thread, FLT: seconds = -1) = MUST pause thread. If seconds is supplied and is non-negative, the runtime MUST automatically resume the thread after that duration. Pausing a thread that is already paused MUST raise a runtime error.
BOOL: PAUSED(THR: thread) = MUST return TRUE when thread is paused and FALSE otherwise.
In the implementation, however, PAUSE(..., seconds=...) spawns a detached timer thread that sleeps then clears the thread's paused flag asynchronously and frees a copy of the THR handle. The worker only observes PAUSED cooperatively at statement boundaries via wait_if_paused(). These asynchronous operations race with the worker finishing and with AWAIT, so scheduling-dependent interleavings can leave PAUSED(...) observed as TRUE (causing REFUTE(PAUSED(...)) to fail) even after AWAIT completes.
According to the specification section 9.1.9:
In the implementation, however,
PAUSE(..., seconds=...)spawns a detached timer thread that sleeps then clears the thread'spausedflag asynchronously and frees a copy of theTHRhandle. The worker only observesPAUSEDcooperatively at statement boundaries viawait_if_paused(). These asynchronous operations race with the worker finishing and withAWAIT, so scheduling-dependent interleavings can leavePAUSED(...)observed asTRUE(causingREFUTE(PAUSED(...))to fail) even afterAWAITcompletes.