29.4 Candidate Executions

A candidate execution of the evaluation of an agent cluster is a Record with the following fields.

Table 81: Candidate Execution Record Fields
Field Name Value Meaning
[[EventsRecords]] A List of Agent Events Records. Maps an agent to Lists of events appended during the evaluation.
[[ChosenValues]] A List of Chosen Value Records. Maps ReadSharedMemory or ReadModifyWriteSharedMemory events to the List of byte values chosen during the evaluation.
[[AgentOrder]] An agent-order Relation. Defined below.
[[ReadsBytesFrom]] A reads-bytes-from mathematical function. Defined below.
[[ReadsFrom]] A reads-from Relation. Defined below.
[[HostSynchronizesWith]] A host-synchronizes-with Relation. Defined below.
[[SynchronizesWith]] A synchronizes-with Relation. Defined below.
[[HappensBefore]] A happens-before Relation. Defined below.

An empty candidate execution is a candidate execution Record whose fields are empty Lists and Relations.