Re: [tlaplus] Modeling leases

Hi Jesse and Igor,

From the description of the algorithm in the Attiya-Welch book, one can see that the algorithm consists of three parts:

1. a broadcast step where process broadcasts its current time,

2. a collection phase where the process collects the messages from other processes and stores intermediate diff values,

3. an evaluation step where the process uses the diffs to compute the adjustment.

Since we assume in this model that the clocks are ticking at the same rate and that messages are always delivered with a delay in the interval [d - u, d], the intermediate diff values and the final adjustment value only depend on d, u, and HC. This fact is captured in Lemma 6.16, which is used to prove Thm. 6.15.

The TLA spec shared by Igor allows the broadcast step to occur spontaneously at any point in time. We can use the property discussed in the above paragraph to argue that it is equivalent to a new spec in which the broadcast step is forced to occur at time 0, for each process. In the new spec, the evaluation step is guaranteed to occur before time d, and thus finite state model checking can be used (picking d, u, HC from finite sets and eliminating time). Model checking is not a good fit for analyzing the new spec: the analysis in the proof for Thm. 6.15 is quite straightforward and verifies the property we are interested in.

The property discussed in the first paragraph allows us to shift events in time so that instead of analyzing a large set of behaviors we can focus our attention on a small set of behaviors. This pattern is a crucial step in the analysis of many real-time models.

Regards,

Abhishek

On Fri, Mar 1, 2024 at 10:30 AM Igor Konnov <igor.konnov@xxxxxxxxx> wrote:

Yes, the idea was to demonstrate how Apalache could naturally check
TLA+ specs over unbounded integers, since SMT solvers are good at it.
In case of TLC, I think you would have to bound the sets Int and Nat.

Best,
Igor

On Thu, Feb 29, 2024 at 2:13 AM A. Jesse Jiryu Davis
<jesse@xxxxxxxxxxxxxxx> wrote:
>
> I've now read the TLA+ spec but I haven't tried to model-check it yet. The spec uses infinite sets such as Int and Nat, it doesn't constrain these to finite sets and it doesn't use the techniques described in Lamport's "Real Time Is Really Simple" to make the state space finite. I don't think spec could be model-checked with TLC. Is this a demonstration of Apalache's advantages over TLC?
>
> On Tue, Feb 27, 2024 at 9:23 AM A. Jesse Jiryu Davis <jesse@xxxxxxxxxxxxxxx> wrote:
>>
>> Thank you!
>>
>> On Tue, Feb 27, 2024 at 8:22 AM Igor Konnov <igor.konnov@xxxxxxxxx> wrote:
>>>
>>> Hi Jesse,
>>>
>>> I used Apalache to check a clock synchronization algorithm a few years
>>> ago. You can have a look at the TLA+ specification [1] and the talk
>>> from the TLA+ Tutorial 2021 [2].
>>>
>>> [1] https://github.com/informalsystems/tla-apalache-workshop/blob/main/examples/clock-sync/ClockSync7.tla
>>> [2] https://youtu.be/NXLJoUKJnDQ?t=5821
>>>
>>> Best,
>>> Igor
>>>
>>> On Mon, Feb 26, 2024 at 1:18 AM A. Jesse Jiryu Davis
>>> <jesse@xxxxxxxxxxxxxxx> wrote:
>>> >
>>> > Hello! Murat Demirbas and I are designing a Raft variant that uses timed leader leases for stronger consistency. We plan to write a TLA+ spec, and it will involve clocks. We're interested in examples in addition to Lamport's "Real Time Is Really Simple" paper. Has anyone worked with time/clocks in TLA+, or could you point us to example specs?
>>> >
>>> > --
>>> > You received this message because you are subscribed to the Google Groups "tlaplus" group.
>>> > To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
>>> > To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFRUCtYYwU8mrQ_3mNqb%2BCYd5xK1ObUuFBRENv34WXMFjFrYNw%40mail.gmail.com.
>>>
>>> --
>>> You received this message because you are subscribed to the Google Groups "tlaplus" group.
>>> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
>>> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CACooHMAmhdEOAXfnvd1y_5q-CfuG3dg%3Dc5wOm-MC5HQjorE%3D7w%40mail.gmail.com.
>
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAFRUCtaeE%2BCeRULB0cx8HeOu%2BoykfetRyyosC9iJ83aJYm4tgw%40mail.gmail.com.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CACooHMCSJM3Y4BsnMyM2%3Dh932KhyFfDv77CkA2A_9c2PEejSMg%40mail.gmail.com.