- Write a spec for the abstract datatype (e.g. set) and then show that your implementation refines it.
- Your spec for the abstract datatype should model the client in addition to the data structure. For a single-threaded data structure, clients serialize their calls; for a concurrent data structure, they do not.
A while back I did this for a concurrent bloom filter I wrote, which is a perfect example since you asked about concurrent sets.
Here's the spec for the abstract datatype:
The three variables "pc", "values_to_insert" and "output" model the clients. Each client first picks a value to insert into the set (PickValue) then hands off control to the data structure to do the actual insert (DoInsert). The data structure returns output to the client in the "output" variable. Since inserts are modeled as a single action, this spec says that inserts should appear to happen atomically.
Here's the spec for the implementation:
There's a wrinkle here: since the bloom filter doesn't store the set explicitly, it's not possible to write a refinement mapping. So instead, my implementation refines a different form of the set specification that only includes the log of inputs/outputs that clients observe. I maintain that this form is equivalent to the simpler form in my first link, although I haven't proven it.