...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of Philosophical Logic >Fine-grained Concurrency with Separation Logic
【24h】

Fine-grained Concurrency with Separation Logic

机译：带有分离逻辑的细粒度并发

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Reasoning about concurrent programs involves representing the information that concurrent processes manipulate disjoint portions of memory. In sophisticated applications, the division of memory between processes is not static. Through operations, processes can exchange the implied ownership of memory cells. In addition, processes can also share ownership of cells in a controlled fashion as long as they perform operations that do not interfere, e.g., they can concurrently read shared cells. Thus the traditional paradigm of distributed computing based on locations is replaced by a paradigm of concurrent computing which is more tightly based on program structure. Concurrent Separation Logic with Permissions, developed by O’Hearn, Bornat et al., is able to represent sophisticated transfer of ownership and permissions between processes. We demonstrate how these ideas can be used to reason about fine-grained concurrent programs which do not employ explicit synchronization operations to control interference but cooperatively manipulate memory cells so that interference is avoided. Reasoning about such programs is challenging and appropriate logical tools are necessary to carry out the reasoning in a reliable fashion. We argue that Concurrent Separation Logic with Permissions provides such tools. We illustrate the logical techniques by presenting the proof of a concurrent garbage collector originally studied by Dijkstra et al., and extended by Lamport to handle multiple user processes.
机译：关于并发程序的推理涉及表示并发进程操纵内存的不相交部分的信息。在复杂的应用程序中，进程之间的内存划分不是静态的。通过操作，进程可以交换存储单元的隐含所有权。另外，进程还可以以受控方式共享单元的所有权，只要它们执行不干扰的操作即可，例如，它们可以同时读取共享的单元。因此，传统的基于位置的分布式计算范例被更紧密地基于程序结构的并发计算范例所取代。由O'Hearn，Bornat等人开发的具有权限的并发分离逻辑能够表示流程之间所有权和权限的复杂转移。我们演示了如何将这些想法用于推理细粒度的并发程序，这些程序不采用显式同步操作来控制干扰，而是协同操作存储单元，从而避免了干扰。关于此类程序的推理具有挑战性，并且必须有适当的逻辑工具才能以可靠的方式进行推理。我们认为具有权限的并发分离逻辑提供了这样的工具。通过展示最初由Dijkstra等人研究并由Lamport扩展以处理多个用户进程的并发垃圾收集器的证明，我们说明了逻辑技术。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号