Ordering, Races, and Atomicity

Ordering model

Rule	Requirement
PL-ORD-01	Each channel provides FIFO ordering per source–destination pair: messages sent from one endpoint to another on one channel are delivered in the order sent, without loss or duplication.
PL-ORD-02	There is no ordering guarantee across channels, and no ordering guarantee between messages of different core–CM pairs. In particular, an A-channel message and a B-channel message in flight at the same time between the same two endpoints may be observed in either order — this is the origin of every race in this chapter.
PL-ORD-03	There is no per-address ordering beyond what PL-ORD-01 provides; ordering of a line’s coherence events is established solely by the CM’s serialization of that line (PL-CM-03).

Useful consequences of PL-ORD-01:

• A core never observes an Invalidate for a line before the Grant that gave it that line: both travel CM → core on channel B, and the CM serializes per line, so the grant is always sent first.

• A Nack sent after an Invalidate to the same core arrives after it (exploited by rule PL-CM-07).

• A forced WriteBack and a subsequent InvAck from the same core arrive at the CM in that order.

Because there is no GrantAck/completion message (unlike TileLink’s channel E), these FIFO properties are what make grants unambiguous: the CM updates its directory at the moment it sends a grant, and FIFO delivery guarantees the core’s view catches up before any later B-channel message for that line arrives.

Atomicity

Rule	Requirement
PL-ORD-04	The CM’s processing of one transaction for one line (directory read, invalidations, memory access, directory update, grant) is atomic with respect to other transactions for that line (PL-CM-03). A requester may therefore treat a received grant as reflecting a consistent, current directory state.

Race conditions

A race is any situation where messages in flight on opposite channels (or from different cores) refer to the same line. PicoLink defines exactly five architecturally visible races and their mandatory resolutions.

Race 1: Dual Upgrade

Two cores both hold a line in S and issue Upgrade concurrently.

Rule

Requirement

PL-RACE-01

The CM shall serve exactly one Upgrade (the winner, chosen per PL-CM-05; the reference implementation picks the lower core index on simultaneous arrival) and shall Nack the other. Serving the winner invalidates the loser (it is a sharer), so by PL-CM-07 the loser receives Invalidate before Nack, and by PL-RACE-03 it has already marked its Upgrade as failed. The loser shall retry with ReadExclusive — not Upgrade, because it no longer holds the line in S (PL-MESI-05) and needs fresh data.

See the corresponding diagram in Message Sequence Diagrams.

Race 2: Upgrade versus ReadShared

Core 0 holds the line in S and issues Upgrade; Core 1 concurrently issues ReadShared for the same line. Both serializations are coherent; the CM picks one (PL-CM-05):

• Upgrade first (the reference CM prioritizes it, since the requester already holds the line): Core 0 receives GrantM (no other sharers to invalidate — Core 1 holds nothing yet) and the directory records M. Core 1’s ReadShared is then a read of a modified line: the CM sends Invalidate to Core 0, receives the forced WriteBack, commits it, acknowledges it, and answers Core 1 from now-current memory.

• ReadShared first: Core 1 is granted S and added to the sharers. Core 0’s Upgrade then finds another sharer: the CM invalidates Core 1, collects its InvAck, and responds GrantM.

Rule	Requirement
PL-RACE-02	Whichever order the CM selects, it shall fully complete the first transaction (including all invalidations and writebacks) before starting the second (PL-CM-03). It shall not Nack the ReadShared in either order (PL-CHAN-04).

Race 3: Invalidate crosses Upgrade

A core in S issues Upgrade. Before the Upgrade reaches the CM (or before the CM serves it), the CM — serving another core’s request — sends Invalidate for the same line. The two messages cross in flight.

Rule	Requirement
PL-RACE-03	A core that receives Invalidate for a line with an Upgrade outstanding shall: respond InvAck normally, transition to I, and mark the outstanding Upgrade as failed. It shall not treat the subsequent Nack as an error, and shall retry the write with ReadExclusive. Symmetrically, the CM shall Nack any Upgrade whose requester is not a recorded holder of the line at service time (stale Upgrade).

Note

The core cannot simply “cancel” the Upgrade — it is already in flight and will be serviced. Rule PL-RACE-03 guarantees both sides independently reach the same conclusion: the core expects a Nack, and the CM produces one.

Race 4: Voluntary WriteBack crosses Invalidate

A core evicts an M line, sending a voluntary WriteBack. Before the WriteBackAck returns, the CM — serving another core’s request for that line — sends Invalidate to the (former) owner. The two messages cross.

Rule

Requirement

PL-RACE-04

The core, now in I with a WriteBack outstanding, shall respond to the crossing Invalidate with InvAck (PL-MESI-06): it holds no data, and the dirty payload is already in flight (PL-MESI-03). The CM shall process the core’s messages in arrival order and classify the WriteBack per PL-TXN-05: If the WriteBack arrives before the CM sends the Invalidate, it is voluntary; the CM commits it, responds WriteBackAck, and — if it then still needs to reclaim the line — proceeds with a directory that no longer lists the core. If the WriteBack arrives after the Invalidate was sent (the crossing case), the CM classifies it as forced: it commits the payload, responds WriteBackAck, and counts the WriteBack as the implicit acknowledgment of the outstanding Invalidate. The InvAck that follows on the same channel (sent by the core per this rule) refers to the same Invalidate; the CM shall accept it as a harmless duplicate acknowledgment and discard it. In both sub-cases exactly one dirty payload reaches memory, the core ends in I, and the CM’s stalled transaction resumes with current data.

Race 5: Invalidate to a silently evicted line

A core silently evicts a clean line (S → I or E → I, PL-MESI-04). The directory still lists the core, so a later transaction causes the CM to send it an Invalidate for a line it no longer holds.

Rule	Requirement
PL-RACE-05	The core shall respond InvAck (PL-MESI-06). The CM shall treat this identically to an InvAck from an actual holder (PL-CM-02). No data is lost: silent eviction is only ever permitted for clean lines, and memory already holds current data (PL-MESI-02).

Deadlock freedom

Protocol-level dependencies form chains such as:

Core1 ReadExclusive → CM Invalidate to Core0 → Core0 InvAck → CM GrantE to Core1

Deadlock freedom follows from three properties, each normative elsewhere in this specification:

1. Unconditional sinking — cores always accept channel B, the CM always accepts channel A, regardless of their own stalled traffic (PL-DEP-01, PL-DEP-02).

2. Bounded outstanding transactions — per-line single outstanding request per core (PL-CHAN-02) and finite txn_id pools bound all queues.

3. Acyclic dependency — every chain has the shape request → (invalidations → acknowledgments) × N → grant; responses never wait on new requests, so chains terminate.