CoLT --- Examples



We evaluated the tool on concurrent set implementations from the book The art of multiprocessor programming by Herlihy and Shavit. We considered an implementation based on fine-grained locking, on optimistic synchronization, on lazy synchronization and on lock-free synchronization. The tool verified linearizability of the first three implementations, and found a known error in the remove method of the lock-free implementation. This error is acknowledged and corrected in the book's errata. CoLT proved that the corrected version is linearizable.

If the answer is that the example is not linearizable, CoLT also returns a visual representation of the trace for inspection by the programmer. The counterexamples are linked to in the tables below. To understand the counterexamples linked to in the tables, one needs to know that nodes 0 and 1 are input nodes to the two methods, and the list itself starts at two.

  • Fine-grained synchronization.
    • Original Java file.
    • Annotated Java file.
    • Results

      Fine-grained results
      Methods M1 loc/pts M2 loc/pts Lin. points Depth Mem (MB) Time (s) Res
      rem || cont 29/2 23/2 No 157 10.2 0.85 Yes
      rem || rem 29/2 29/2 No 141 8.3 0.46 Yes
      rem || add 29/2 26/2 No 303 18.1 2.4 Yes
  • Optimistic synchronization.
    • Original Java file.
    • Annotated Java file.
    • Results

      Optimistic results
      Methods M1 loc/pts M2 loc/pts Lin. points Depth Mem (MB) Time (s) Res
      add || rem 40/3 38/2 No 110 37.6 5.8 Yes
      cont || cont 30/3 30/3 No 150 37.6 6.9 Yes
      rem || rem 38/3 38/3 No 130 36.2 6.3 Yes
  • Lazy synchronization.
    • Original Java file.
    • Annotated Java file.
    • Results

      Lazy results
      Methods M1 loc/pts M2 loc/pts Lin. points Depth Mem (MB) Time (s) Res
      rem || rem 36/3 36/3 No 164 20.1 2.68 Yes
      rem || add 36/3 34/3 No 164 26.3 3.51 Yes
      cont || rem 36/3 6/1 No 136 13.2 1.28 Yes
      rem1 || add1 36/3 34/3 No 137 24.2 3.17 No
      rem2 || rem2 34/3 34/3 No 143 17.9 2.18 No
  • Lock-free synchronization.
    • Original Java file.
    • Annotated Java file.
    • Results

      Lock-free results
      Methods M1 loc/pts M2 loc/pts Lin. points Depth Mem (MB) Time (s) Res
      cont || cont 9/2 9/2 No 98 6.4 0.25 Yes
      rem || rem 34/3 34/3 Yes 95 77.6 8.08 No
      remC || remC 34/3 34/3 Yes 268 1908.3 605 Yes
      add || remC 35/3 34/3 No ? out ? ?
      add || remC 35/3 34/3 Yes 267 1550.3 577 Yes
      add || cont 35/3 9/2 No 400 18984.1 5700 Yes