Re: [tlaplus] Verifying concurrent data structures

[Jones Martins <jonesmvc@xxxxxxxxx>]

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/25fffdb8-9414-4b9b-826d-414a333458dcn%40googlegroups.com.