Re: [tlaplus] Verifying concurrent data structures

[Dmytro Ivanov <dmytro@xxxxxxxxxxxxxx>]

I've implemented something similar to one of my employers:
- We had existing lockfree MPMC stack/queue/etc data structures in C.
- I've converted existing code to PlusCal almost 1-to-1 to best of my ability. There were some nitpicks regarding how PlusCal implements return values, so I took some liberties. But important part is from a view of sequential consistency, most if not all sequence points were preserved. That is a bit weak guarantee as obviously every C sequence point potentially compiles to multiple instructions, so one could go and model instructions directly if that is what required. But most lockfree algorithms are not relying on specific ordering of instructions between threads, they more relying on ordering of sequence points, so overall it's fairly ok.
- On top of that I've added a "test program" written also in PlusCal that emulates 2-3+ threads and tries to add/remove elements from the data structure, test program keeps a separate set of "correct" elements. And it compares reference to result of algorithm.
- Then I've limited generation counters (common feature in lockfree algorithms to resolve ABA) to something small like 100.
- Running TLC then finds all possible states, and proves that algorithm is correct, with exception of generation counter wrap around (if one thread is stuck and another wraps around generation counter, then you still arrive at ABA).

Generally it's great for sequential consistency code. My next goal was to try different relaxed memory models, but I've moved to other stuff ..

On Thursday, December 23, 2021 at 1:19:15 AM UTC+1 jone...@xxxxxxxxx wrote:

Thank you, Markus for the example, and Calvin, for your examples and explanations!

I looked for data structure specs in the tlaplus/examples repo on Github, but I couldn't find any. Maybe I didn't search right?

Also, Markus, OpenAddressing.tla seems like a nice addition to the tlaplus/examples repository, don't you think?

Regards,

Jones

On Wednesday, 22 December 2021 at 15:10:44 UTC-3 Markus Alexander Kuppe wrote:

On 12/21/21 3:29 PM, Jones Martins wrote:
> Hello, everyone
>
> Since TLA+ can also verify (and prove) correctness of algorithms,
> protocols, etc., I wonder how to verify data structures. When modelling
> a sequential data structure compared to a concurrent data structure, how
> should one go about specifying it?
>
>  For example, let's say I implemented an abstract Set specification
> with "Add", "Remove" and "Contains" actions. How do I prove correctness?
> What about a concurrent Set?
>
> Thanks
>
> Jones


https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/src/tlc2/tool/fp/OpenAddressing.tla
is a spec of a concurrent, lock-free set (no deletion).

Markus

-- 
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/d1e62261-5e38-47c8-95f0-ecb526f45bb8n%40googlegroups.com.