Certifying Concurrent Programs Using Transactional Memory

来源 :计算机科学技术学报(英文版) | 被引量 : 0次 | 上传用户:jia343212539
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
Transactional memory (TM) is a new promising concurrency-control mechanism that can avoid many of the pitfalls of the traditional lock-based techniques. TM systems handle data races between threads automatically so that programmers do not have to reason about the interaction of threads manually. TM provides a programming model that may make the development of multi-threaded programs easier. Much work has been done to explore the various implementation strategies of TM systems and to achieve better performance, but little has been done on how to formally reason about programs using TM and how to make sure that such reasoning is sound. In this paper, we focus on the semantics of transactional memory and present a proof-carrying code (PCC) system for reasoning about programs using TM . We formalize our reasoning with respect to the TM semantics, prove its soundness, and use examples to demonstrate its effectiveness.
其他文献
警务实战训练的开展离不开教学法的运用,“贴近实战”是考量警务实战训练水平高低的标尺,在诸多教学法中,情景模拟教学法是最符合“贴近实战”要求的教学法,通过设置模拟警情,可以
随着我国教育信息化的推进,数字化的学习资源日益丰富,新的学习方式不断出现,要适应新背景下教育对教师的要求,教师必须具备良好的信息素养。本文从信息化教育背景下教师的角色转
班主任是一个班集体的核心。班主任工作的优劣直接影响着班集体的形成。同时,班主任的素质对学生综合素质的培养具有重要的影响。良好班集体的形成,是班主任与学生共同努力的结
写作是重点中的重点,所以在冲刺阶段复习时如何提高学生用英语获取信息、处理信息、分析和解决问题的能力;逐步培养用英语进行思维和表达的能力;成为了我们首要解决问题。本人通
在新课程改革的形势下要求一个合格的高中物理教师,决不能“教书匠”式地“照本宣科”,而要在教学中不断思考,不断学习,与时共进。新课程提倡培养学生独立思考能力、发现问题与解
社会主义核心价值观是社会主义核心价值体系的内核和精髓,也是高校教书育人的重要职责。本文主要分析了高校建设社会主义核心价值观的重要性和迫切性,大学生在社会主义核心价值
在新课标的背景下,初中思想政治课特别强调情感、态度、价值观这一教学目标。在初中思想政治课教学中,如何有效地采取情感引导策略,从而帮助学生树立正确的情感、态度、价值观目
感情是心灵的火花,一本书、一句话、一件事都可触发学生心灵的震撼,在传递正能量,重塑信仰的今天,结合教学实际,通过具体事例感染学生,激发其爱国之情、树立其报国之志、促使其努力
通过剖析因学生素质、招生规模、授课时间发生变化而引起的难教问题,找到破解难教办法,从而实现教学质量不下降,教学教法步步新的真正目的。
Particle layers tend to build up on walls in many filtration and separation processes, calling for periodic removal in order to keep the apparatus running. Impo