Determinacy with Priorities up to Clocks

1. Il Problema

Il lavoro nasce dalla necessità di colmare il divario tra la teoria della concorrenza classica di Milner (CCS) e le esigenze dei linguaggi di programmazione sincrona deterministica (come Esterel o SL).

• Limiti della Confluenza di Milner: Nella teoria originale di CCS, la proprietà di confluenza (che garantisce la determinatezza e l'assenza di condizioni di gara) non è chiusa rispetto alla composizione parallela. Per preservare la confluenza, Milner richiede condizioni di "separazione dei sort" (sort separation), che impediscono la condivisione diretta di canali tra processi.
• Incapacità di Modellare la Memoria Condivisa: Questo approccio fallisce nel modellare sistemi con memoria condivisa e aggiornamenti distruttivi (come una cella di memoria con lettori e scrittori). In questi scenari, processi come un lettore e uno scrittore che competono per la stessa risorsa non sono confluenti secondo la definizione classica, anche se il sistema è deterministico grazie a meccanismi di priorità o gestione dell'assenza.
• Mancanza di Causalità e Reazione all'Assenza: La teoria di Milner non riesce a esprimere in modo compositivo la causalità, la memoria condivisa multi-thread e la "reazione all'assenza" (un concetto fondamentale nei linguaggi sincroni dove un'azione avviene solo se un certo segnale non è presente).

2. Metodologia

Gli autori introducono CCSspt, un'estensione del CCS che integra tre elementi chiave per gestire la programmazione sincrona:

1. Orologi (Clocks): Un singolo orologio $\sigma$ (estendibile a multi-orologio) che sincronizza i processi. I processi possono avere un "orizzonte temporale" (clock horizon) che definisce se partecipano alla sincronizzazione globale o operano in modo asincrono.
2. Priorità e Blocco (Priorities & Blocking): Le azioni sono protette da priorità. Un'azione può essere bloccata se un'azione di priorità superiore è disponibile nello stesso orizzonte temporale.
3. Transizioni Strategiche (Strategic Transitions): Invece delle transizioni standard $P \xrightarrow{\alpha} Q$, il sistema utilizza transizioni strategiche $P \xrightarrow{\alpha:B[\iota]} Q$, dove:
   • $\alpha$ è l'azione.
   • $B$ (Blocking) è una relazione che specifica quali azioni bloccano $\alpha$ entro un certo orizzonte temporale.
   • $\iota$ (Prediction) è una funzione che predice quali azioni sono in competizione con $\alpha$ all'interno dell'orizzonte temporale.

Concetto Chiave: Coerenza (Coherence)
Gli autori ridefiniscono la confluenza introducendo il concetto di Coerenza. Questa nuova nozione sostituisce:

• La determinatezza con l'osservabilità (Observable): Due transizioni con la stessa azione visibile devono portare a stati congruenti, a meno che non siano "osservabili" come competitori tramite le etichette strategiche.
• La distinzione delle etichette con l'indipendenza (Independence): Due transizioni sono indipendenti solo se non si bloccano a vicenda (rispetto alle relazioni di blocco $B$).

La Coerenza richiede che per ogni coppia di transizioni indipendenti, esista una riconvergenza (Diamond Property) che sia monotona rispetto alle relazioni di blocco e di previsione.

3. Contributi Chiave

• Estensione Compositiva del CCS: Il paper presenta un'estensione formale del CCS che supporta nativamente la programmazione sincrona, la memoria condivisa e la reazione all'assenza senza perdere la composizionalità.
• Definizione di Coerenza: Viene proposta una nuova proprietà semantica che generalizza la confluenza di Milner. A differenza della confluenza classica, la coerenza è preservata dalla composizione parallela ($P|Q$) e dalla restrizione ($P\setminus A$) senza richiedere condizioni di separazione dei sort.
• Gestione della Memoria Condivisa Deterministica: Il sistema permette di modellare celle di memoria con lettori multipli e scrittori singoli in modo deterministico. Le priorità e i meccanismi di blocco risolvono le condizioni di gara (race conditions) a livello semantico, garantendo che il sistema sia coerente anche quando i singoli componenti non lo sono secondo la teoria classica.
• Semantica "Up-to-Clocks": L'uso della funzione di previsione $iA^*$ (che considera le azioni fino all'orizzonte dell'orologio, non solo quelle immediate) permette di modellare l'astrazione micro-macro step tipica dei linguaggi sincroni come Esterel. Questo evita problemi di non-determinismo che sorgerebbero con previsioni basate solo sulle azioni immediate ($iA$).

4. Risultati Principali

• Teorema di Preservazione (Theorem 1): Se due processi $P_1$ e $P_2$ sono coerenti, allora la loro composizione parallela $P_1 | P_2$ e la loro restrizione $P \setminus A$ sono anch'esse coerenti. Questo è un risultato fondamentale che supera i limiti della teoria di Milner, dove la preservazione richiedeva vincoli stringenti sulla separazione dei canali.
• Unicità della Forma Normale: I processi coerenti sono "determinati" sotto le azioni silenziose ($\tau$). Ogni processo coerente riduce a una forma normale unica (a meno di congruenza), garantendo l'assenza di condizioni di gara interne.
• Modellazione di Esterel: Il sistema dimostra di poter codificare costrutti complessi di linguaggi sincroni come Esterel (es. l'esempio ABRO) in modo compositivo, gestendo correttamente la logica "Read-Before-Write" e la reazione all'assenza di segnali.
• Blocco Auto-Referente (Self-Blocking): Il sistema introduce il concetto di azioni che si bloccano da sole in presenza di più concorrenti (es. una scrittura che si blocca se ci sono due scrittori), permettendo una semantica di concorrenza vera (true-concurrency) che non è esprimibile in CCS standard o in estensioni prioritarie precedenti come CPG.

5. Significato e Impatto

Questo lavoro rappresenta un avanzamento significativo nella teoria dei processi algebrici per la concorrenza:

• Ponte Teorico: Fornisce un fondamento teorico solido che unisce la logica della concorrenza (CCS) con la semantica dei linguaggi di programmazione sincrona (Esterel, SL), risolvendo il problema storico di come modellare la memoria condivisa in modo deterministico e compositivo.
• Superamento delle Limitazioni di Milner: Dimostra che la confluenza può essere generalizzata per includere sistemi con memoria condivisa e priorità, eliminando la necessità di vincoli di separazione dei sort che limitavano l'espressività dei modelli precedenti.
• Fondamento per Linguaggi Futuri: La nozione di "Coerenza" e l'uso di etichette strategiche basate sugli orologi offrono un nuovo paradigma per la progettazione di linguaggi di coordinamento e sistemi distribuiti che richiedono sia determinismo che flessibilità nella sincronizzazione.
• Confronto con Altri Formalismi: Il paper posiziona CCSspt come più espressivo di approcci precedenti (come Sπ o SPL) e lo confronta con il framework BIP, suggerendo che le priorità "up-to-clocks" offrono una capacità espressiva superiore per la gestione della concorrenza globale.

In sintesi, il paper propone una nuova teoria della determinatezza ("Coerenza") che rende possibile la modellazione compositiva di sistemi sincroni complessi con memoria condivisa, risolvendo problemi aperti nella teoria della concorrenza di Milner.