CIVL Verification of Lock-free Hash Set

This problem was part of the VerifyThis 2022 verification competition. The competition took place on April 2, 2022, in München, Germany, as part of the ETAPS conference. The competition consists of three challenges. Each challenge describes some algorithms, including some pseudo-code, and a list of properties to verify. Participants use any platform of their choice to implement, specify, and verify the algorithms. Each challenge lasts one hour and 50 minutes.

The problem description is here. The problem is inspired by the “world’s simplest lock-free hash table”, from Jeff Preshing’s blog. The problem describes a lock-free concurrent hash set that supports adding an element and membership test. The algorithms use an atomic compare-and-swap operation.

Here are the properties to prove:

  1. empty(n) creates an empty set with capacity n
  2. member(k) == true, if insert(k) has been executed before (and returned true)
  3. member(k) == false, if no insert(k) that returned true can have been executed
  4. termination
  5. every key is contained in the table at most once
  6. if insert returns false, the table is full

Here is the CIVL solution I came up with during the competition:

The CIVL code follows the C++-like pseudocode given in the problem description very closely. I used CIVL to verify certain properties involving two concurrently executing threads with an upper bound (N) on the capacity of the hash set. Each thread chooses two keys nondeterministically and inserts those keys into the set. Then membership tests are performed. The output (excerpted):

Leave a Reply