正文
图
.5.
独占
（左）和读
/
锁定（右）合约
这是一个相当粗暴的解决方案，因为这意味着排除合约中的任何并发交互。然而，从一个角度来看，合约作为并发对象的观点是很明显的，请看我们的类比：帐号是线程。实际上，如图5 所示，通过对合约施加特定所有权规则类似于通过对Thread进行明确检查来增强其Java对等体。currentThread（）.getId（）。
现在让我们尝试通过设计具有更详细访问权限的计数器来进一步推动帐户和线程之间的比较。我们将确保只要存在“有兴趣”的帐户（即“线程”）使其值不可变（因为内部逻辑可能依赖其不变性），则不允许其他方修改它。同样，如果目前正好有一方拥有修改合约的唯一许可，则不得允许其他方阅读。这种同步问题的解决方案是通过名称读/锁定[6]，这在并发社区中是众所周知的。其实现需要跟踪当前正在读取和写入共享对象的线程，所以在执行读/写操作之前，线程应该明确获取相应的权限，然后在完成后释放它。
图5的右侧部分显示了读/写锁定合约实现的基本部分。两个新领域，跟踪目前活跃的读者和作家。新的修饰符canRead和canWrite将被用于省略的get和set操作。最后，只要在系统中没有活动写入器，AcquReadRock允许其调用者获取锁定，通过读取器映射注册。
我们可以看到，以线程方式类比是十分有效的。我们提出了一些解决可能的同步问题的方案，可以从并发文献中逐字逐句地进行。所提出的解决方案的唯一缺点是它是相当整体的事实：合约现在将数据结构（即，计数器）的功能与同步原语（即，锁）的功能相结合。我们将在第5节中讨论提高实现模块性的可能途径。
关于正式推理和验证的注意事项。关于许可账户和所有状态分离访问的正式推理是共享内存并发文献中长期研究的主题（参见例如[8] 的概述）。正式主义，如并发分离逻辑和[30]分数/计数权限[6]提供了一种灵活的方式来定义抽象所有权规则，并验证一个特定的实现是否忠实地遵循。例如，我们的读/写锁合约可以通过Bornat等人的正式的权限模型证明是安全的（即禁止并发修改）[6]。
5
讨论
5.1
合约的编写
在第4节中考虑的锁定合约“模式”具有重大的延伸：其设计是非模块化的。也就是说，锁定机构是由合约本身而不是由第三方数据实施的。这与软件工程的良好做法不同，建议将同步原语（例如普通和可重入锁）实现为独立库，可用于管理访问客户端特定的资源。
但是一旦锁定逻辑被解除合约之外，关于合约行为的推理就显得更加困难，因为为了证明其内部不变量的保存，需要了解锁定协议的属性，例如编者的独特性，这在合约之外。换句话说，合约的验证不能再以孤立的方式进行，需要建立一个模型，允许对与其他严格指定的合约交互的合约进行推理。解除合约逻辑的想法不只是我们这样认为的，而且在合约开发中是至关重要的。例如，同样的想法被提倡作为通过引入和额外的间接层次来实施Ethereum可升级合约的一种方式[11]。拥有由任何一方可以援引的另一个合约的“合约工厂”构成了与证明高阶并发对象的安全属性（即，与其他对象一起作用）类似的验证挑战[19]。
