Isabelle files for verification of a hybrid transactional mutex lock

This page contains Isabelle theory files for proving correctness of hybrid transactional memory in a modular fashion, leveraging the TMS2 specification and Lesani et al's results, these proofs establish opacity of two novel hybrid versions of the Dalessandro et al.'s transactional mutex lock . Modularisation is based on a concept we refer to as open I/O automata. Download the theory files here. The zip file consists of two folders: <i> naive</i>, a simple implementation and proof, where the fast and slow path both synchronise on the same global variable, and <i> 2-Counter</i>, an improved implementation and proof, where the slow- and fast-path transactions synchronise on different variables, allowing more concurrency. The proofs require Isabelle 2016. If you encounter a problem loading Seq.thy, please make sure imports is set to "../HOLCF". This is a problem with the new Isabelle distribution.

本页面提供用于以模块化方式证明混合事务内存正确性的Isabelle理论文件，本工作依托TMS2规范与Lesani等人的研究成果，上述证明验证了Dalessandro等人提出的两种新型混合版本事务互斥锁的不透明性（opacity）。本次证明的模块化设计基于我们称之为开放I/O自动机（open I/O automata）的概念。请在此处下载该理论文件。该压缩包包含两个文件夹：<i>naive</i>（朴素版）：一种简易实现与证明方案，其快速路径与慢速路径均在同一全局变量上完成同步；以及<i>2-Counter</i>（双计数器版）：一种优化后的实现与证明方案，其慢速路径与快速路径事务可在不同变量上实现同步，进而支持更高并发度。上述证明需在Isabelle 2016环境下运行。若在加载Seq.thy时遇到问题，请确保将导入路径设置为"../HOLCF"，该问题系新版Isabelle发行版所导致。