diff --git a/spec.html b/spec.html index b41fe83840..c345fe85b4 100644 --- a/spec.html +++ b/spec.html @@ -36057,9 +36057,10 @@
A WaiterList is a semantic object that contains an ordered list of those agents that are waiting on a location (_block_, _i_) in shared memory; _block_ is a Shared Data Block and _i_ a byte offset into the memory of _block_.
+A WaiterList is a semantic object that contains an ordered list of those agents that are waiting on a location (_block_, _i_) in shared memory; _block_ is a Shared Data Block and _i_ a byte offset into the memory of _block_. A WaiterList object also optionally contains a Synchronize event denoting the previous leaving of its critical section.
+Initially a WaiterList object has an empty list and no Synchronize event.
The agent cluster has a store of WaiterList objects; the store is indexed by (_block_, _i_). WaiterLists are agent-independent: a lookup in the store of WaiterLists by (_block_, _i_) will result in the same WaiterList object in any agent in the agent cluster.
-Operations on a WaiterList—adding and removing waiting agents, traversing the list of agents, suspending and notifying agents on the list—may only be performed by agents that have entered the WaiterList's critical section.
+Operations on a WaiterList—adding and removing waiting agents, traversing the list of agents, suspending and notifying agents on the list, setting and retrieving the Synchronize event—may only be performed by agents that have entered the WaiterList's critical section.
The abstract operation GetWaiterList takes two arguments, a Shared Data Block _block_ and a nonnegative integer _i_. It performs the following steps:
The abstract operation LeaveCriticalSection takes one argument, a WaiterList _WL_. It performs the following steps: