Determinacy with Priorities up to Clocks

1. Problem Statement

The paper addresses a fundamental limitation in Milner's Calculus of Communicating Systems (CCS) regarding the modeling of deterministic concurrent systems, particularly those found in synchronous programming languages like Esterel.

• The Limitation of Classical Confluence: In Milner's theory, a process is "determinate" if identical actions lead to congruent states. To ensure this property is preserved under parallel composition, Milner introduced "confluence." However, classical confluence requires that any two distinct transitions must eventually reconverge to congruent states.
• The Conflict with Shared Memory & Synchrony: This classical definition fails for systems involving:
  1. Shared Memory: Processes with shared state (e.g., a memory cell with readers and writers) often exhibit race conditions where distinct actions (read vs. write) lead to non-congruent states. Classical confluence forbids this, yet such systems are deterministic if priorities resolve the race.
  2. Reaction to Absence: Synchronous languages rely on "reaction to absence" (e.g., if an action does not occur in a clock cycle, execute an alternative). Milner's CCS cannot express this causality compositionally.
  3. Sort Separation: Milner's preservation of confluence under parallel composition requires a "Separation Condition" (disjoint action sets), which prevents modeling shared resources where multiple threads access the same label.

The authors argue that existing extensions (like $S\pi$ or SPL) fail to capture Esterel's global consistency and reaction to absence compositionally.

2. Methodology

The authors propose a new process algebra, $CCS_{spt}$ (Single-clock CCS with Priorities and Time), which extends Milner's CCS with priorities and clocks.

A. Syntax and Semantics

• Strategic Transitions: Instead of standard transitions $P \xrightarrow{\alpha} Q$, the system uses strategic transitions $P \xrightarrow{\alpha:B[\iota]} Q$.
  • $\alpha$: The action label.
  • $B$ (Blocking): A set of constraints $(C, L)$ indicating that action $\alpha$ is blocked if any action in set $L$ occurs within clock horizon $C$.
  • $\iota$ (Prediction): A function mapping clock horizons to sets of competing actions. It predicts which actions are syntactically available to compete with $\alpha$ up to the next clock tick.
• Clock Horizons: Processes have a horizon $C \in \{\{\}, \{\sigma\}\}$.
  • $\{\sigma\}$: Synchronous processes that must synchronize on every clock tick.
  • $\{\}$: Asynchronous processes.
• Constructivity: The prediction function $iA^*_C(P)$ is defined conservatively (up-to clocks), meaning it includes all actions syntactically present in the process up to the next clock, ensuring monotonicity.

B. Key Mechanisms

1. Priority-Guarded Actions: An action $\alpha:L.P$ can only proceed if no action in $L$ is available. This allows modeling "Read-Before-Write" policies.
2. Self-Blocking: A process can block itself. For example, a write action can be defined to block if another writer is present, preventing race conditions without requiring external sort separation.
3. Reaction to Absence: By using $\tau$-prefixes with blocking sets (e.g., $\tau:\{a\}.Q$), the system can detect if action $a$ is absent in the current clock cycle and trigger $Q$ accordingly.

3. Key Contributions

A. The Concept of "Coherence"

The authors introduce Coherence as a generalization of Milner's confluence. Coherence replaces two classical requirements with new ones based on strategic labels:

1. Observability (replacing Determinacy): Instead of requiring congruent states for identical actions, the system requires that if two transitions have different outcomes, the competing actions must be observable in the prediction sets of the transitions. This allows non-congruent states if the race is resolved by priority.
2. Independence (replacing Distinctness): Two transitions are "independent" (and thus require reconvergence) only if they are mutually non-blocking.
   • If a read action is blocked by a writer (due to priority), they are not independent; no reconvergence is required.
   • If two writers compete for a single write slot, the write action is self-blocking, making the transitions dependent and preventing the race.

B. The Diamond Property for Strategic Transitions

The authors define a Diamond Property (DP) for coherent processes. If two independent transitions diverge, they must reconverge to congruent states with monotonic blocking and prediction relations ($B' \sqsubseteq B$ and $\iota' \sqsubseteq \iota$). This ensures that as the system evolves, constraints do not arbitrarily tighten or loosen in a way that breaks determinacy.

C. Preservation Theorem

Theorem 1 states that coherence is preserved under:

• Parallel Composition ($P | Q$): Unlike Milner's confluence, this does not require sort separation. Shared memory and multi-cast communication are allowed.
• Restriction ($P \setminus A$): Coherence is preserved when restricting labels.

4. Results and Examples

• Shared Memory Modeling: The paper demonstrates how to model a memory cell with multiple readers and writers.
  • Readers: Can synchronize on the same label without blocking each other (non-blocking).
  • Writers: Use self-blocking to ensure only one writer proceeds.
  • Priority: A write action blocks a read action if both are present, ensuring data consistency.
• Reaction to Absence: The system successfully encodes Esterel's "abort" and "watchdog" patterns. For instance, a:P + \tau:\{a\}:Q executes Q if a is not present in the current clock cycle.
• Expressiveness: The authors prove that $CCS_{spt}$ cannot be compositionally encoded into standard CCS. The "self-blocking" mechanism creates a true-concurrency semantics that standard CCS cannot replicate, as standard parallel composition preserves all transitions of components, whereas $CCS_{spt}$ can block transitions based on the presence of other components.

5. Significance

• Bridging Theory and Practice: The paper provides a rigorous semantic foundation for synchronous programming languages (like Esterel) within a process algebra framework, solving the long-standing issue of modeling shared memory and reaction to absence compositionally.
• Generalization of Confluence: It significantly extends Milner's theory by showing that determinacy can be achieved without strict sort separation, provided that priorities and clock-based blocking are used to resolve races.
• New Semantic Paradigm: The introduction of "strategic labels" with blocking and prediction functions offers a novel way to handle scheduling and causality in concurrent systems, moving beyond immediate enabling to "up-to-clocks" enabling.
• Comparison with BIP: The authors note that while BIP (Behavior, Interaction, Priority) handles interactions, it relies on local priorities based on immediate actions. $CCS_{spt}$'s "up-to-clocks" priorities and self-blocking capabilities offer a more expressive model for global consistency in synchronous systems.

In summary, the paper establishes Coherence as the correct notion of determinacy for synchronous, shared-memory concurrent systems, using $CCS_{spt}$ to formally prove that such systems can be composed without losing determinacy, even in the presence of shared resources and complex priority schemes.