diff --git a/spec.html b/spec.html index 846548f32f..5d848dfaaa 100644 --- a/spec.html +++ b/spec.html @@ -37250,9 +37250,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.
-Each WaiterList has a critical section that controls exclusive access to that WaiterList during evaluation. Only a single agent may enter a WaiterList's critical section at one time. Entering and leaving a WaiterList's critical section is controlled by the abstract operations EnterCriticalSection and LeaveCriticalSection. 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.
+Each WaiterList has a critical section that controls exclusive access to that WaiterList during evaluation. Only a single agent may enter a WaiterList's critical section at one time. Entering and leaving a WaiterList's critical section is controlled by the abstract operations EnterCriticalSection and LeaveCriticalSection. 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:
EnterCriticalSection has contention when an agent attempting to enter the critical section must wait for another agent to leave it. When there is no contention, FIFO order of EnterCriticalSection calls is observable. When there is contention, an implementation may choose an arbitrary order but may not cause an agent to wait indefinitely.
The abstract operation LeaveCriticalSection takes one argument, a WaiterList _WL_. It performs the following steps:
The abstract operation NotifyWaiter takes two arguments, a WaiterList _WL_ and an agent signifier _W_. It performs the following steps:
The abstract operation SynchronizeEventSet takes one argument, a candidate execution _execution_. It performs the following steps:
-The abstract operation HostEventSet takes one argument, a candidate execution _execution_. It performs the following steps: