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

Re: [tlaplus] Verifying concurrent data structures

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?



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).


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.