Re: [tlaplus] Verifying concurrent data structures

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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/e4109462-f7eb-98a6-d641-c9fb89cc7d50%40lemmster.de.