Verification with Spin

• Modeled the software transaction implementation in Promela

• Low-level model – every memory operation represented

  • details in the paper

• Spin used 16G of memory to check the implementation within a 6-version 2-object scope.

Notes: