Here are two versions of clock synchronization, based on the algorithm described in: Dolev, Halpern, Simons, and Strong, "Fault-tolerant clock synchronization". In Proceedings of the 3rd ACM Symposium on Principles of Distributed Computing, 1984, pp. 89-102.

The essence of the algorithm is that all processes wait for their internal clocks to reach the next synchronization time. The first process to reach it sends a message to the others, who then update their clocks.

### Without Fault Tolerance#

As a simplification, we can remove fault tolerance from the algorithm. In this formulation, each process simply waits for the round to end, either due to its internal timer or an external message. There is no need to track time within a round, or to check messages for validity beyond ensuring they belong to the correct round.

```{-
Run a single clock process
Arguments:
* process id
* the mailbox for this process
* list of mailboxes for all other processes
-}
def process(n, self, others) =
def round(ET) =
println(n + ": " + ET) >>
map(lambda (m) = m.put(ET), others) >>
round(ET+1)
round(1)

{-
Start a set of clock processes
Arguments:
* list of mailboxes for processes to be created
* list of mailboxes for processes already created
* next process id
-}
def start([], _, _) = stop
def start(m:ms, ms', n) = process(n, m, append(ms, ms')) | start(ms, m:ms', n+1)

-- Start four processes
val buffers = map(ignore(Buffer), range(1,10))
start(buffers, [], 1)```

### With Fault Tolerance#

The complete algorithm implements fault tolerance by checking that synchronization messages are within a delta of the local clock.

```{-
A simple clock synchronization demo,
based on the algorithm described in:
Dolev, Halpern, Simons, and Strong,
"Fault-tolerant clock synchronization".
In Proceedings of the 3rd ACM Symposium
on Principles of Distributed Computing,
1984, pp. 89-102.
-}

-- Number of clock ticks per synchronization period
val PER = 10
-- Maximum drift (delta between clocks) over a period
val D = 900
-- Minimum real-time duration of a clock tick
val t = 100
-- Maximum drift (delta between clocks) per tick
val d = D / PER
-- Type of messages:
-- Tick: internal clock tick
-- Synch(time, [id]): synchronization message signed
-- with a list of process ids
type Message = Tick() | Synch(_, _)

{-
Run a single clock process
Arguments:
* process id
* the mailbox for this process
* list of mailboxes for all other processes
-}
def process(n, self, others) =
{- Send a message to all other processes -}
def send(msg) = map(lambda (m) = m.put(msg), others)
{- Simulate a clock for this process -}
def clock() =
Rtimer(t+random(d)) >>
self.put(Tick()) >>
clock()
{- Message-processing loop -}
{- Internal clock tick -}
{- External synchronization event -}
def on(Synch(T, s)) =
if T = ET && ET - length(s)*D < C
then send(Synch(T, n:s)) >>
println(n + ": " + ET) >>
if C = ET
then send(Synch(ET, [n])) >>
println(n + ": " + ET) >>
else on(self.get())
{- Goal expression -}

{-
Start a set of clock processes
Arguments:
* list of mailboxes for processes to be created
* list of mailboxes for processes already created
* next process id
-}
def start([], _, _) = stop
def start(m:ms, ms', n) = process(n, m, append(ms, ms')) | start(ms, m:ms', n+1)

-- Start four processes
val buffers = map(ignore(Buffer), range(1,10))
start(buffers, [], 1)```

Only authorized users are allowed to upload new attachments.