Scholarlink

Compared to semantics with preemptively executing threads, ones with cooperative threads permit easier specification of atomicity in concurrent programs. We introduce a semantics of cooperative programs, and a simulation notion compatible with rely-guarantee proofs. We prove our simulation composes in parallel and sequentially, and that it can establish a standard trace-based notion of refinement.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

A Rely-Guarantee-Based Simulation for Cooperative Semantics

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Kevin Tran,
  • Johannes Åman Pohjola,
  • Rob Sison,
  • Gerwin Klein

摘要

Compared to semantics with preemptively executing threads, ones with cooperative threads permit easier specification of atomicity in concurrent programs. We introduce a semantics of cooperative programs, and a simulation notion compatible with rely-guarantee proofs. We prove our simulation composes in parallel and sequentially, and that it can establish a standard trace-based notion of refinement.