[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Verifying concurrent data structures

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?


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

is a spec of a concurrent, lock-free set (no deletion).


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.