Determinacy with Priorities up to Clocks

Titel: Determinacy with Priorities up to Clocks

Auteurs: Luigi Liquori, Michael Mendler, Claude Stolze
Context: PLACES 2026 (EPTCS 444)

---

1. Het Probleem

Het paper adresseert een fundamentele beperking in de klassieke theorie van concurrentie, zoals geformuleerd door Robin Milner in zijn Calculus of Communicating Systems (CCS).

• Determinisme en Confluëntie: In CCS is determinisme gedefinieerd als de eigenschap dat dezelfde actie vanuit een staat altijd leidt tot congruente vervolgstaten. Om dit te combineren met parallelle compositie, introduceerde Milner het concept van confluëntie. Echter, deze theorie is onvoldoende voor moderne synchrone programmeertalen (zoals Esterel) en systemen met gedeeld geheugen.
• Beperkingen van Milner's Theorie:
  1. Sorte-scheiding: Milner's theorie vereist strikte "sort separation" (disjuncte acties) om confluëntie te behouden bij parallelle compositie. Dit maakt het onmogelijk om gedeeld geheugen (waarbij meerdere processen op dezelfde variabele lezen/schrijven) op een samenstellende (compositional) manier te modelleren zonder data-races.
  2. Afwezigheidsreactie: Synchrone talen zoals Esterel hebben de capaciteit om te reageren op de afwezigheid van een signaal binnen een klokcycllus. Milner's CCS kan dit niet expressief modelleren.
  3. Niet-determinisme: Bestaande processalgebra's zijn inherent niet-deterministisch, terwijl synchrone talen vaak deterministische semantiek vereisen voor voorspelbaarheid.

Het doel is om een uitbreiding van CCS te creëren die zowel synchrone timing (klokken) als prioriteiten ondersteunt, zodat deterministische systemen met gedeeld geheugen en afwezigheidsreactie op een samenstellende manier kunnen worden gedefinieerd.

---

2. Methodologie

De auteurs introduceren een nieuwe processalgebra genaamd CCSspt (CCS with Priorities up to Clocks). De kern van de methodologie ligt in de uitbreiding van de standaard getransitieerde systemen (LTS) met strategische labels.

A. Syntaxis en Semantiek van CCSspt

• Acties: Het systeem onderscheidt tussen rendezvous-acties (handshakes, $a, \bar{a}$) en broadcast-acties (klokken, $\sigma$).
• Horizonten (Clock Horizons): Processen hebben een horizon:
  • $\{\sigma\}$: Synchroon proces; moet synchroniseren op elke tik van de klok.
  • $\emptyset$: Asynchroon proces; neemt niet deel aan de klok.
• Prioriteiten: Acties kunnen worden voorafgegaan door een set van prioriteiten $L$ (bijv. $\alpha:L.P$). Dit betekent dat actie $\alpha$ alleen kan plaatsvinden als geen enkele actie in $L$ kan synchroniseren binnen de huidige klokhorizon.

B. Strategische Transities

In plaats van de standaard overgang $P \xrightarrow{\alpha} Q$, gebruiken de auteurs strategische transities:
$$P \xrightarrow{\alpha : B[\iota]} Q$$

• $\alpha$: De uitgevoerde actie.
• $B$ (Blocking): Een verzameling blokkerende constraints. Een transitie is geblokkeerd als er een concurrente actie bestaat die in de prioriteitsset $L$ valt binnen de relevante horizon.
• $\iota$ (Prediction): Een voorspellingsfunctie die aangeeft welke acties binnen de horizon $P$ potentieel concurreren met $\alpha$.

De auteurs definiëren een Labelled Transition System (LTS) met regels voor:

• Compositie (Com): Synchronisatie van rendezvous en klokken.
• Parallelle uitvoering (Par): Asynchrone stappen zijn alleen mogelijk als de voorspelling van de partner de blokkering niet activeert.
• Som (Sum): Selectie van een prefix gebaseerd op concurrentie met andere opties in dezelfde thread.

C. Het Concept van "Coherence" (Coherentie)

De auteurs vervangen Milner's klassieke definities van determinisme en confluëntie door een nieuw concept: Coherentie.

• Observability (Observatie): Een proces is observeerbaar als concurrerende acties (die tot verschillende staten leiden) zichtbaar zijn in elkaars voorspelling ($\iota$). Dit lost het probleem op van meerdere lezers die dezelfde actie uitvoeren.
• Independence (Onafhankelijkheid): Twee transities zijn onafhankelijk als ze niet elkaars blokkering activeren.
• Diamond Property (DP): Voor elke paar onafhankelijke transities moet er een reconvergentie zijn naar congruente staten.
• Resultaat: Een coherent proces reduceert tot een unieke normale vorm (onder $\tau$-transities), zelfs in aanwezigheid van gedeeld geheugen en prioriteiten.

---

3. Belangrijkste Bijdragen

1. CCSspt Algebra: Een nieuwe processalgebra die prioriteiten koppelt aan klokhorizonten ("up-to clocks"), waardoor het mogelijk is om synchrone scheduling te modelleren.
2. Strategische Labels: Een formalisme dat blokkering en voorspelling integreert in de transitielabels, wat een fijnmazigere controle op concurrentie mogelijk maakt dan traditionele prioriteitssystemen.
3. Definitie van Coherentie: Een generalisatie van Milner's confluëntie die werkt voor systemen met gedeeld geheugen en prioriteiten, zonder de beperkende "sort separation" conditie.
4. Behoudstheorema (Preservation Theorem): Het bewijs dat coherentie behouden blijft onder parallelle compositie ($P|Q$) en restrictie ($P\setminus A$). Dit is een sterk resultaat omdat Milner's theorie hiervoor extra voorwaarden vereiste.
5. Modellering van Esterel-achtige constructies: Het paper toont aan dat systemen zoals Esterel's ABRO en gedeeld geheugen met "Read-Before-Write" prioriteiten op een samenstellende manier kunnen worden gemodelleerd.

---

4. Resultaten

• Unieke Normalisatie: Het paper bewijst (Lemma 1) dat coherent processen deterministisch zijn onder stilte-acties ($\tau$); ze reduceren altijd naar een unieke normale vorm.
• Oplossing voor Data Races: Door gebruik te maken van "self-blocking" (een actie blokkeert zichzelf als er meerdere instanties zijn) en prioriteiten, kunnen data-races in gedeeld geheugen worden opgelost zonder dat het systeem niet-deterministisch wordt.
  • Voorbeeld: Een schrijver ($w$) heeft prioriteit boven een lezer ($r$). Als er twee schrijvers zijn, blokkeert de actie omdat de prioriteitset de concurrentie detecteert.
• Expressiviteit: Het paper toont aan dat CCSspt niet composioneel kan worden ingebed in standaard CCS. De "self-blocking" eigenschap en de voorspelling tot aan de klokhorizon ($iA^*$) creëren een echte concurrentie-semantiek die niet in eerdere prioriteitssystemen (zoals CPG) voorkomt.
• Afwezigheidsreactie: Het systeem kan de afwezigheid van een actie binnen een cyclus detecteren (bijv. "als $a$ niet mogelijk is, doe $b$"), wat essentieel is voor synchrone talen.

---

5. Significatie

De bijdrage van dit paper is significant voor de theorie van concurrente systemen en synchrone programmeertalen:

• Brug tussen Theorie en Praktijk: Het biedt een formele basis die de kloof overbrugt tussen Milner's abstracte concurrentietheorie en de praktische eisen van synchrone talen (zoals Esterel) die determinisme en gedeeld geheugen vereisen.
• Versterking van Confluëntie: Het introduceert "Coherentie" als een robuuster alternatief voor confluëntie dat minder restrictief is (geen sorte-scheiding nodig) en beter past bij moderne architecturen.
• Nieuwe Semantische Kader: De introductie van "up-to clocks" prioriteiten en voorspelling via $iA^*$ biedt een nieuwe manier om scheduling en concurrentie te analyseren, wat leidt tot een "waarachtige concurrentie" (true-concurrency) semantiek.
• Toekomstgericht: De auteurs wijzen op de potentie voor uitbreiding naar meerdere klokken, bisimulatie en integratie met andere coördinatieparadigma's zoals BIP (Behavior, Interaction, Priority).

Kortom, het paper levert een fundamentele uitbreiding van de processalgebra-theorie die het mogelijk maakt om deterministische, synchrone systemen met complexe interacties (gedeeld geheugen, prioriteiten) op een wiskundig onderbouwde en samenstellende manier te specificeren.