# Synpatick: Coherence and Determinacy with Priorities and Clocks

Claude Stolze, Luigi Liquori, Michael Mendler

► To cite this version:

Claude Stolze, Luigi Liquori, Michael Mendler. Synpatick: Coherence and Determinacy with Priorities and Clocks. Synchron 2025 - 32th International Open Workshop on Synchronous Programming, Nov 2025, Aussois, France. hal-05459053v2

HAL Id: hal-05459053

https://inria.hal.science/hal-05459053v2

Submitted on 16 Jan 2026

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons CC BY 4.0 - Attribution - International License
# Coherence and Determinacy with Priorities and Clocks

Claude Stolze

joint work with Michael Mendler and Luigi Liquori

Otto-Friedrich Universität Bamberg
Centre INRIA d'Université Côte d'Azur
Motivations and context

* Aim: present the semantics of **Synchronous Programming (SP)** in the framework of **Process Algebras**

- Make SP more appealing to other communities interested in concurrent programming and concurrency theory

- Develop and study a shallow encoding of (multiclock) SP languages in process algebras

* Our basic framework: CCS with clocks and priorities (CCS<sup>spt</sup>)

- Previous (async.) systems with clocks [Hoare]

- Previous (async.) systems with priorities [Camilleri & Winskel, Phillips]

* CCS<sup>spt</sup> combines clocks and priorities in a synchronous setting
# What is CCS<sup>spt</sup>?

* CCS<sup>spt</sup> is a process calculus with

- CCS (rendezvous) actions for communication [Milner]

- CSP (broadcast) actions for clocks [Hoare]

- Priorities for constructive scheduling [Camilleri & Winskel, Phillips]

- **NEW**: multiclock (GALS, ...)

- **NEW**: both reduction semantics and labelled transition semantics

* A first glance of CCS<sup>spt</sup> was presented in Synchron 2023 (Kiel), an encoding single-clock Esterel was presented in Synchron 2024 (Bamberg)
Syntax

<table>
  <tbody>
    <tr>
      <td rowspan="4">P, Q</td>
      <td>::=</td>
      <td>M</td>
      <td>thread</td>
    </tr>
    <tr>
      <td>|</td>
      <td>p</td>
      <td>process name, p &isin; I</td>
    </tr>
    <tr>
      <td>|</td>
      <td>P | Q</td>
      <td>parallel composition</td>
    </tr>
    <tr>
      <td>|</td>
      <td>P \ A</td>
      <td>restriction, A &sube; A.</td>
    </tr>
    <tr>
      <td rowspan="3">M, N</td>
      <td>::=</td>
      <td>0<sub>C</sub></td>
      <td>hiding, C &sube; C</td>
    </tr>
    <tr>
      <td>|</td>
      <td>&alpha; : L &middot; P</td>
      <td>inactive process prefix, L &sube; L</td>
    </tr>
    <tr>
      <td>|</td>
      <td>M + N</td>
      <td>sum</td>
    </tr>
  </tbody>
</table>

Example:

User $\stackrel{\text{def}}{=} \sigma.\sigma.\overline{\text{ctrlc}}.0_{\sigma}$

Prog $\stackrel{\text{def}}{=} \text{hello:ctrlc.}\sigma.\text{Prog} + \text{ctrlc.}0_{\sigma}$

Main $\stackrel{\text{def}}{=} (\text{User} | \text{Prog}) / \sigma \setminus \text{ctrlc}$

Process names have arguments
# Dealing with multiple clocks

* `clocks(P)` is the set of clocks which are **active for** (read “free in”) *P*

* *P* has to synchronize on `clocks(P)`, but not on other clocks

* `clocks(0<sub>C</sub>) = C`: it blocks clocks **only** in set *C*, and does not care about other clocks

* Example: $0_{\sigma} | \rho.P$ can perform $\rho.P$, but $0_{\rho} | \rho.P$ is stuck

* With multiclocks:

* $\sigma.0_{\{\sigma, \rho'\}} | \rho.0_{\rho} | \rho'.0_{\rho'}$ can perform either $\sigma$ or $\rho$, but not $\rho'$

* A process *P* is **well-defined** (noted `WD(P)`) if `clocks(P)` is constant throughout its execution

* Example: $a.\sigma.0_{\sigma} + b.0_{\sigma}$ is well-defined

* Counter-example: $a.\rho.0_{\sigma}$ is **not** well-defined. Indeed, if it performs *a* and then $\rho$, it loses the clock $\rho$

* Another counter-example: $a.0_{\sigma} + b.0_{\rho}$
# Scheduling with multiple clocks

* Each process has to be scheduled according to its clocks and the blocking sets of its actions

* There are 2 issues to consider

* Issue 1: $a:b.0_\sigma | \rho.b.0_\rho$ cannot perform $a$. Indeed, it is in concurrence with $\rho.b.0_\rho$ which can perform $b$ inside a $\sigma$-cycle

- In order to schedule the actions of $P$ in a process $P | Q$, we have to consider the actions of $Q$ **up to** clocks($P$). This set is called $iA_{\text{clocks}}^*(P)(Q)$

* Issue 2: Scheduling a non deterministic choice + has to consider immediate conflicts.

Ex: $a:b.0_\sigma | (c.b.0_\sigma + \bar{a}.0_\sigma)$ cannot perform $a$, but the $\tau$-transition would make $b$ disappear, so we can do it.

However: $a:b.0_\sigma | (\bar{b}.0_\sigma + \bar{a}.0_\sigma)$ should not be able to perform either $a$ or $\tau$ (immediate preemption)

- In that case, we consider the simple initial actions $iA(P)$, i.e. the actions a process can do immediately
# Labelled Transition System

$$ \begin{array}{l} \text{Example:} \\ \mathit{User} \ \stackrel{\text{def}}{=} \ \sigma.\sigma.\overline{\mathit{ctrlc}}.0_{\sigma} \\ \mathit{Prog} \ \stackrel{\text{def}}{=} \ \mathit{hello}:\mathit{ctrlc}.\sigma.\mathit{Prog} + \mathit{ctrlc}.0_{\sigma} \\ \mathit{Main} \ \stackrel{\text{def}}{=} \ (\mathit{User} | \mathit{Prog}) / \sigma \setminus \mathit{ctrlc} \end{array} $$

* LTS: $P \xrightarrow{\alpha} \iota_Q$ means $P$ can become $Q$ with **action** $\alpha$ and the **blocking constraints** $B$, and the **prediction information** $\iota$ (omitted)

$$ \mathit{Prog} \xrightarrow{\overline{\mathit{hello}}(\sigma, \mathit{ctrlc})} \sigma.\mathit{Prog} \\ \mathit{User} | \sigma.\mathit{Prog} \xrightarrow{(\sigma, \{\})} \sigma.\overline{\mathit{ctrlc}}.0_{\sigma} | \mathit{Prog} $$

* **Blocking constraints**: each action has a set of contributing threads, each one with its set of clocks and a set of blocking actions

$$ \text{Ex:} \quad \sigma:\{a, b\}.0_{\sigma} | \sigma:b.0_{\sigma, \rho} | \sigma:c.0_{\sigma, \rho'} \xrightarrow{\sigma(\sigma, \{a, b\}), (\sigma, \rho), \{b\}, (\sigma, \rho'\}, c)} 0_{\sigma} | 0_{\sigma, \rho} | 0_{\sigma, \rho'} $$
# Term Rewriting System

* The Term Rewriting System explains **how** processes reduce internally:

hello.hello | Main — hello | (User | σ.Prog) / σ \ ctrlc

* We can reduce only if we know everything about the blocking actions, e.g.

$$a:b | \bar{a}$$

cannot reduce, because I don't know if we can do b, but

$$(a:b | \bar{a}) \setminus b$$

can reduce
Equivalence

$$M_1 + (M_2 + M_3) \equiv (M_1 + M_2) + M_3$$

$$M_1 + M_2 \equiv M_2 + M_1$$

$$M + O_{\text{clocks}}(M) \equiv M$$

$$P_1 | (P_2 | P_3) \equiv (P_1 | P_2) | P_3$$

$$P_1 | P_2 \equiv P_2 | P_1$$

$$P | 0\{\} \equiv P$$

$$P \setminus A \equiv P$$

$$P \setminus A_1 \setminus A_2 \equiv P \setminus (A_1 \cup A_2)$$

$$P | (Q \setminus A) \equiv (P | Q) \setminus A$$

$$0_{C_1} / C_2 \equiv 0_{C_1} - C_2$$

$$P / C \equiv P$$

$$P / C_1 / C_2 \equiv P / (C_1 \cup C_2)$$

$$P \setminus A / C \equiv P / C \setminus A$$

$$P | (Q / C) \equiv (P | Q) / C$$

$$p \equiv P$$

$$\text{if } \mathcal{L}(P) \cap (A \cup \bar{A}) = \{\}$$

$$\text{if } \mathcal{L}(P) \cap (A \cup \bar{A}) = \{\}$$

$$\text{if } \mathcal{L}(P) \cap C = \{\}$$

$$\text{if } \mathcal{L}(P) \cap C = \{\}$$

$$\text{if } p \stackrel{\text{def}}{=} P$$
Reduction semantics

Definition : allows($i, C, L$) $\stackrel{\text{def}}{=} i(C) \cap \bar{L} = \{\}$

$$ \frac{\text{allows}(iA^*_-(R), \text{clocks}(P), L) \quad L \subseteq C \cup A \cup \bar{A}}{((\tau:LP + M) | R) / C \setminus A \longrightarrow (P | R) / C \setminus A} \quad (R-\text{Tau}) $$

$$ \frac{L \cup L' \subseteq C \cup A \cup \bar{A} \quad \text{allows}(iA^*_-(R) \cup (iA(N) - \{\bar{a}\}), \text{clocks}(P), L) \quad \text{allows}(iA^*_-(R) \cup (iA(M) - \{a\}), \text{clocks}(Q), L')}{((a:LP + M) | (\bar{a}:L'.Q + N) | R) / C \setminus A \longrightarrow (P | Q | R) / C \setminus A} \quad (R-\text{Com}) $$

$$ \begin{gathered} \bigcup_i L_i \subseteq C \cup A \cup \bar{A} \qquad \sigma \in C \qquad \sigma \notin \text{clocks}(R) \\ \forall i, \text{allows}(iA^*_-(R) \cup (\bigcup_{j \neq i} iA(M_j) - \{\sigma\}), \text{clocks}(P_i), L_i) \end{gathered} $$

$$ \frac{(\sigma:L_1.P_1 + M_1) | \dots | (\sigma:L_n.P_n + M_n) | R) / C \setminus A \longrightarrow (P_1 | \dots | P_n | R) / C \setminus A}{(R-\text{Clk})} $$
## Labelled Transition System

Definition : allows($i, B$) $\stackrel{\text{def}}{=} \forall (C, L) \in B, i(C) \cap \bar{L} = \{\}$

$$ \alpha: L \cdot P \frac{\alpha}{\{(\text{clocks}(P), L)\}_{i\{\}}^\alpha} P \quad (\text{Act}) $$

$$ \frac{M_1 \xrightarrow{\alpha} P_1}{M_1 + M_2 \xrightarrow{\alpha} i_1 \cup (iA(M_2) - \{\alpha\})} P \quad (\text{Sum}_1) $$

$$ \frac{P_1 \xrightarrow{\ell} P'_1 \quad P_2 \xrightarrow{\bar{\ell}} P'_2 \quad \text{allows}(i_1, B_2) \quad \text{allows}(i_2, B_1)}{P_1 | P_2 \xrightarrow{\frac{\ell}{B_1 \cup B_2}} i_1 + i_2 \quad P'_1 | P'_2} \quad (\text{Com}) $$

$$ \frac{P \xrightarrow{\alpha} P' \quad \text{allows}(iA^-(Q), B) \quad \alpha \notin \text{clocks}(Q)}{P | Q \xrightarrow{\frac{\alpha}{B} + iA^+(Q)} P' | Q} \quad (\text{Par}_1) $$

Restriction acts as in CCS, and hiding acts as in CSP
# Properties

* The Term Rewriting System and the Labelled Transition System are in harmony, i.e. their semantics coincide

## Lemma (Harmony)

$$ P \rightarrow Q \text{ iff } P \xrightarrow{\tau} B \xrightarrow{\iota} Q' \equiv Q \\ \text{for some } \iota, Q', B \text{ such that } \forall (C, L) \in B, L = \{\} $$
# Examples with multiple clocks

* Looping on clocks in C:

$$halt_C \stackrel{\text{def}}{=} \sum_{\sigma \in C} \sigma.halt_C$$

* Get a string from keystrokes (at most one keystroke per $\rho$-cycle):

$$ \text{GetString} \stackrel{\text{def}}{=} \overline{\text{return.}string.halt}_{\rho} + \text{key:}return.\rho.\text{GetString} + \rho:\{\text{return, key}\}.\text{GetString} $$

* Getting a string in a $\sigma$-cycle:

$$ \text{GetString} | (\text{string}.\sigma.Q_1 + \sigma:\text{string}.Q_2) $$

* This is deterministic, thanks to priorities

* As GetString does not do $\sigma$-transition, $iA^*_{\{\sigma\}}(\text{GetString})$ contains string, so it blocks the $\sigma$ transition

* $\rho$ is temporarily a "refinement" of $\sigma$ [cf. Gemünde]
# Examples with multiple clocks

* GetString with a bit of asynchrony:

$$ \text{GetString} \stackrel{\text{def}}{=} \text{return.}(\overline{\text{string.}}\text{0}_{\{}}|\text{halt}_{\sigma}) \\ + \text{key:}return.\rho.\text{GetString} \\ + \rho:\{\text{return, key}\}.\text{GetString} $$

* Getting a string asynchronously (in the spirit of GALS):

$$ \text{Bridge} \stackrel{\text{def}}{=} \text{string.}\overline{\text{ok}}.\text{halt}_{\sigma} + \sigma.\text{Bridge} $$

* Bridge sends the $\overline{\text{ok}}$ signal in the same cycle it received the string

* Bridge does not follow the maximal clock progress principle, it is not deterministic either

* $P \stackrel{\text{def}}{=} \text{ok.}\sigma.P' + \sigma:\text{ok}.P$

* We can consider

`` `GetString | Bridge | P` ``
# Conclusion and Future Work

* Define a **reasonable** Church-Rosser property (Coherence)

* a property studied by Milner in Communication and Concurrency

<figure><img src="image_2.png" /></figure>

<table><tr><td>10.5 Stratification of process logic</td><td>221</td></tr><tr><td>11 Determinacy and Confluence</td><td>231</td></tr><tr><td>11.1 Determinacy</td><td>232</td></tr><tr><td>11.2 Preserving determinacy</td><td>235</td></tr><tr><td>11.3 Confluence</td><td>237</td></tr><tr><td>11.4 Preserving confluence</td><td>243</td></tr></table>

* The top (rendez-vous) transitions in the CR diagram **should not** be mutually exclusive

* Formally, $\forall (C, L) \in B_2, \alpha \notin L$ and $\forall (C, L) \in B_1, \beta \notin L$

* Ex: in $a:b + b$, the a- and b-transition are mutually exclusive

* Policies could help us ensure coherence

* Implementing a software prototype (WIP)