Verifiably Correct Transactional Memory.

可验证正确的事务内存。

基本信息

  • 批准号:
    EP/R032351/1
  • 负责人:
  • 金额:
    $ 51.78万
  • 依托单位:
  • 依托单位国家:
    英国
  • 项目类别:
    Research Grant
  • 财政年份:
    2018
  • 资助国家:
    英国
  • 起止时间:
    2018 至 无数据
  • 项目状态:
    已结题

项目摘要

Multi-core computing architectures have become ubiquitous over the last decade. This has been driven by the demand for continual performance improvements to cope with the ever-increasing sophistication of applications, combined with physical limitations on chip designs, whereby speedup via higher clock speeds has become infeasible. The inherent parallelism that multi-core architectures entail offers great technical opportunities, however, exploiting these opportunities presents a number of technical challenges.To ensure correctness, concurrent programs must be properly synchronised, but synchronisation invariably introduces sequential bottlenecks, causing performance to suffer. Fully exploiting the potential for concurrency requires optimisations to consider executions at low levels of abstraction, e.g., the underlying memory model, compiler optimisations, cache-coherency protocols etc. The complexity of such considerations means that checking correctness with a high degree of confidence is extremely difficult. Concurrency bugs have specifically been attributed to disasters such as a power blackout in north eastern USA, Nasdaq's botched IPO of Facebook shares, and the near failure of NASA's Mars Pathfinder mission. Other safety-critical errors have manifested from using low-level optimisations, e.g., the double-checked locking bug and the Java Parker bug.This project improves programmability of concurrent programs through the use of transactional memory (TM), which is a concurrency mechanism that makes low-level optimisations available to general application programmers. TM is an adaptation of transactions from databases. TM operations are highly concurrent (which improves efficiency), yet manage synchronisation on behalf of a programmer to provide an illusion of atomicity. Thus, by using TM, the focus of a programmer switches from what should be made atomic, as opposed to how atomicity should be guaranteed. This means concurrent systems can be developed in a layered manner (enabling a separation of concerns).The attractive set of features that TM promises means that TM implementations are increasingly being incorporated into mainstream systems (hardware and software). Since the adaptation of transactions from database theory in the mid 1990s, software TM implementations are now available for all major programming languages. Recent advances include experimental features in compilers such as G++ 4.7 that directly enable compilation of transactional code; standardisation work to include TM within C++ is ongoing. There is extensive research interest in hybrid TM within both academia and industry to make best use of, for example, TM features in Intel's Haswell/Broadwell and IBM's Blue Gene/Q processors.The high level of complexity, yet wide-scale applicability of TM means that implementations must be formally verified to ensure dependability and reliability. This project addresses some of the main challenges surrounding TM, and takes the key steps necessary to facilitate wide-scale adoption. Namely, we deliver theoretical advances in our understanding of TM correctness; methodological advances in verification techniques for TM; and pragmatic advances via the development of application-aware TM designs. Verification tools will support each of these steps. We therefore set the following objectives:O1. Develop foundations for TM correctness (atomicity and interaction guarantees) under different execution models and relate these to client correctness.O2. Mechanically verify correctness of TM implementations, and develop principled proof techniques.O3. Design TM implementations that provide better performance under current and future multi-core hardware.O4. Develop tool support to simplify mechanised verification of TM and automated checking of client programs that use them.Overall, we will improve the dependability, performance, and flexibility of TM implementations.
在过去的十年中,多核计算架构变得无处不在。这是由于对持续改进性能的需求,以应对日益复杂的应用程序,加上芯片设计的物理限制,通过更高的时钟速度进行加速已变得不可行。多核体系结构固有的并行性提供了巨大的技术机会,然而,利用这些机会带来了许多技术挑战。为了确保正确性,并发程序必须正确同步,但同步总是会引入顺序瓶颈,导致性能下降。充分利用并发性的潜力需要优化来考虑低抽象级别的执行,例如底层存储器模型、编译器优化、高速缓存一致性协议等。这些考虑的复杂性意味着以高度的置信度检查正确性是极其困难的。并发漏洞被明确地归因于灾难,如美国东北部的停电,纳斯达克拙劣的Facebook股票首次公开募股,以及美国国家航空航天局的火星探路者任务几乎失败。该项目通过使用事务内存(TM)来提高并发程序的可编程性,这是一种并发机制,使普通应用程序程序员可以进行低级优化。TM是对来自数据库的事务的改编。TM操作是高度并发的(这提高了效率),但仍代表程序员管理同步,以提供原子性的错觉。因此,通过使用TM,程序员的关注点从应该使之原子化的内容转变,而不是应该如何保证原子性。这意味着并发系统可以以分层的方式开发(实现关注点分离)。TM承诺的一组吸引人的功能意味着TM实现正越来越多地被纳入主流系统(硬件和软件)。自20世纪90年代中期从数据库理论中改编事务以来,软件TM实现现在可用于所有主要编程语言。最近的进展包括编译器中的实验性功能,如G++4.7,它直接支持事务代码的编译;将TM包括在C++中的标准化工作正在进行中。学术界和工业界对混合TM有着广泛的研究兴趣,以充分利用英特尔的Haswell/Broadwell和IBM的Blue Gene/Q处理器中的TM功能。TM的高度复杂性和广泛适用性意味着必须对实现进行正式验证,以确保可靠性和可靠性。该项目解决了围绕TM的一些主要挑战,并采取了必要的关键步骤来促进广泛采用。也就是说,我们在我们对TM正确性的理解方面取得了理论上的进步,在TM验证技术上取得了方法学上的进步,并通过开发具有应用意识的TM设计来实现了实用上的进步。核查工具将支持上述每个步骤。因此,我们制定了以下目标:O1。在不同的执行模式下建立TM正确性(原子性和交互保证)的基础,并将其与客户正确性联系起来。机械地验证TM实现的正确性,并开发原则性证明技术。设计在当前和未来的多核硬件下提供更好性能的TM实现。开发工具支持,以简化TM的机械化验证和使用它们的客户端程序的自动检查。总体而言,我们将提高TM实施的可靠性、性能和灵活性。

项目成果

期刊论文数量(10)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
Verifying correctness of persistent concurrent data structures: a sound and complete method
验证持久并发数据结构的正确性:一种健全且完整的方法
  • DOI:
    10.1007/s00165-021-00541-8
  • 发表时间:
    2021
  • 期刊:
  • 影响因子:
    1
  • 作者:
    Derrick J
  • 通讯作者:
    Derrick J
Owicki-gries reasoning for C11 RAR
C11 RAR 的 Owicki-Gries 推理
Defining and Verifying Durable Opacity: Correctness for Persistent Software Transactional Memory
Integrating Owicki-Gries for C11-Style Memory Models into Isabelle/HOL
将 C11 型内存模型的 Owicki-Gries 集成到 Isabelle/HOL 中
  • DOI:
    10.1007/s10817-021-09610-2
  • 发表时间:
    2021
  • 期刊:
  • 影响因子:
    0
  • 作者:
    Dalvandi S
  • 通讯作者:
    Dalvandi S
Modularising Verification Of Durable Opacity
持久不透明性的模块化验证
{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ monograph.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ patent.updateTime }}

John Derrick其他文献

Proving Opacity of a Pessimistic STM
证明悲观 STM 的不透明性
  • DOI:
    10.4230/lipics.opodis.2016.35
  • 发表时间:
    2016
  • 期刊:
  • 影响因子:
    0
  • 作者:
    Simon Doherty;Brijesh Dongol;John Derrick;Gerhard Schellhorn;Heike Wehrheim
  • 通讯作者:
    Heike Wehrheim
On using data abstractions for model checking refinements
  • DOI:
    10.1007/s00236-007-0042-3
  • 发表时间:
    2007-03-07
  • 期刊:
  • 影响因子:
    0.500
  • 作者:
    John Derrick;Heike Wehrheim
  • 通讯作者:
    Heike Wehrheim
Formally based tool support for model checking Erlang applications

John Derrick的其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

{{ truncateString('John Derrick', 18)}}的其他基金

Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT)
安全可靠的高级架构并发编程 (COVERT)
  • 批准号:
    EP/X015114/1
  • 财政年份:
    2023
  • 资助金额:
    $ 51.78万
  • 项目类别:
    Research Grant
Verifiably correct concurrency abstractions
可验证正确的并发抽象
  • 批准号:
    EP/R018936/1
  • 财政年份:
    2018
  • 资助金额:
    $ 51.78万
  • 项目类别:
    Research Grant
Verifying concurrent algorithms on Weak Memory Models
验证弱内存模型上的并发算法
  • 批准号:
    EP/M017044/1
  • 财政年份:
    2015
  • 资助金额:
    $ 51.78万
  • 项目类别:
    Research Grant
Verifying Concurrent Lock-free Algorithms
验证并发无锁算法
  • 批准号:
    EP/J003727/1
  • 财政年份:
    2012
  • 资助金额:
    $ 51.78万
  • 项目类别:
    Research Grant
Higher-order Refinement Techniques for Model Driven Architecture
模型驱动架构的高阶细化技术
  • 批准号:
    EP/G031711/1
  • 财政年份:
    2009
  • 资助金额:
    $ 51.78万
  • 项目类别:
    Research Grant

相似海外基金

SHF: Medium: Provably Correct, Energy-Efficient Edge Computing
SHF:中:可证明正确、节能的边缘计算
  • 批准号:
    2403144
  • 财政年份:
    2024
  • 资助金额:
    $ 51.78万
  • 项目类别:
    Standard Grant
I-Corps: Vision analysis system using inferred three-dimensional data to analyze and correct a user’s pose in relation to 3D space
I-Corps:视觉分析系统,使用推断的三维数据来分析和纠正用户相对于 3D 空间的姿势
  • 批准号:
    2403992
  • 财政年份:
    2024
  • 资助金额:
    $ 51.78万
  • 项目类别:
    Standard Grant
In vivo precision genome editing to correct genetic disease
体内精准基因组编辑以纠正遗传疾病
  • 批准号:
    10771419
  • 财政年份:
    2023
  • 资助金额:
    $ 51.78万
  • 项目类别:
The development of Machine Learning methods to correct data responses from low-cost sensors to improve agricultural productivity and air quality data accuracy.
开发机器学习方法来纠正低成本传感器的数据响应,以提高农业生产力和空气质量数据的准确性。
  • 批准号:
    10081002
  • 财政年份:
    2023
  • 资助金额:
    $ 51.78万
  • 项目类别:
    Collaborative R&D
Defining the Potential of Gene Therapy to Correct Motor Disabilities of CTNNB1 Syndrome Using in Vivo Mouse and in Vitro Human Cell Models
利用体内小鼠和体外人类细胞模型确定基因疗法纠正 CTNNB1 综合征运动障碍的潜力
  • 批准号:
    10809254
  • 财政年份:
    2023
  • 资助金额:
    $ 51.78万
  • 项目类别:
A correct-by-construction approach to approximate computation
一种近似计算的构造修正方法
  • 批准号:
    EP/Y000455/1
  • 财政年份:
    2023
  • 资助金额:
    $ 51.78万
  • 项目类别:
    Research Grant
A theorem prover for the correct development of reconfigurable systems
正确开发可重构系统的定理证明者
  • 批准号:
    23K11048
  • 财政年份:
    2023
  • 资助金额:
    $ 51.78万
  • 项目类别:
    Grant-in-Aid for Scientific Research (C)
Identification, development and application of novel neuroserpin inhibitors to correct the NGF deficiency in the Alzheimer's disease pathology
新型神经丝氨酸蛋白酶抑制剂的鉴定、开发和应用以纠正阿尔茨海默病病理学中的 NGF 缺陷
  • 批准号:
    490333
  • 财政年份:
    2023
  • 资助金额:
    $ 51.78万
  • 项目类别:
    Operating Grants
Developing microwave epiphysiodesis to correct limb length discrepancies
开发微波骨骺固定术以纠正肢体长度差异
  • 批准号:
    10804031
  • 财政年份:
    2023
  • 资助金额:
    $ 51.78万
  • 项目类别:
Using machine learning to correct for the impact of detector effects in top measurements on ATLAS
使用机器学习来校正 ATLAS 顶部测量中探测器效应的影响
  • 批准号:
    574378-2022
  • 财政年份:
    2022
  • 资助金额:
    $ 51.78万
  • 项目类别:
    University Undergraduate Student Research Awards
{{ showInfoDetail.title }}

作者:{{ showInfoDetail.author }}

知道了