Verifiably correct high-performance concurrency libraries for multi-core computing systems
可验证正确的多核计算系统高性能并发库
基本信息
- 批准号:EP/N016661/1
- 负责人:
- 金额:$ 12.52万
- 依托单位:
- 依托单位国家:英国
- 项目类别:Research Grant
- 财政年份:2016
- 资助国家:英国
- 起止时间:2016 至 无数据
- 项目状态:已结题
- 来源:
- 关键词:
项目摘要
The benefits of fast computer systems are clear - improving performance allows more sophisticated applications to be developed. Speed-up via higher processor clock speeds, however, reached a physical upper limit in the early 2000s, with power-dissipation becoming a major issue. Hardware designers have therefore switched to multicore processors with fixed clock speeds, where speed-up is achieved by including several cores in a single processor. Multicore processors are now pervasive in all aspects of computing, from cluster servers and desktops to low-power mobile devices.A multicore processor efficiently executes concurrent programs comprising multiple threads by allowing several computations to take place simultaneously in the different cores. These threads communicate via synchronised access and modification of shared resources stored in shared memory. While some problems (coined embarrassingly parallel problems) are naturally able to take advantage of multicore computing, the majority require clever management of thread synchronisation that is difficult to achieve. Moreover, modern architectures have forced programmers to understand intricate details of the hardware/software interface in addition to concurrency issues within the programs they develop.Within a multicore processor, each processing core has access to a local buffer that acts as a temporary cache - any writes stored in a local buffer are not visible to other cores until the buffer is flushed. For efficiency reasons, multicore architectures implement so-called relaxed-memory models, where read and write events within a single thread may take effect in shared memory out-of-order, leading to behaviours that may not be expected by a programmer. Restoring correctness requires manual introduction of "fence" instructions in a program's code, which is a non-trivial task - under-fencing leads to incorrect behaviours, while overfencing leads to inefficient programs. Therefore, as Shavit states, "The advent of multicore processors as the standard computing platform will force major changes in software design." There is a large international effort in both academia and industry to make better use of multicore processing, ranging from new foundational and theoretical underpinnings to the development of novel abstractions, tool support, engineering paradigms, etc.In this project, we aim to simplify system development via practical solutions that are highly performant (to increase efficiency), verifiably correct (to ensure dependability) and cope with relaxed-memory models (as used by modern hardware). In particular, we develop efficient "concurrent objects" that provide abstractions from the low-level hardware interface and manage thread synchronisation on behalf of a programmer. Concurrent objects are to ultimately become part of a programming language library - some languages e.g., Java already offer basic concurrent objects as part of their standard library - hence are highly applicable.The objects we deliver will take advantage of relaxed memory models. Here, it is well known that correctness conditions that are too strict (e.g., linearizability) are themselves becoming a barrier to efficiency. We therefore begin by developing new theoretical foundations in the form of relaxed correctness conditions that match relaxed memory models. A hierachy of different conditions will be developed, enabling one to easily determine the relative strengths of each condition. These conditions will be linked to a contextual notion of refinement to provide a basis for substitutability in client programs. This provides a basis for more efficient, verifiably correct, concurrent objects for relaxed memory models. We will focus on developing concurrent data structures (e.g., stacks, queues, deques) for the TSO memory model. Their verification will be mechanised in the KIV theorem prover to eliminate human error in verification, which in turn improves dependability.
快速计算机系统的好处是显而易见的-提高性能可以开发更复杂的应用程序。然而,通过更高的处理器时钟速度实现的加速在21世纪初达到了物理上限,功耗成为一个主要问题。因此,硬件设计人员转向了具有固定时钟速度的多核处理器,其中通过在单个处理器中包含多个内核来实现加速。多核处理器已经广泛应用于计算的各个方面,从集群服务器和台式机到低功耗的移动的设备,多核处理器通过允许多个计算在不同的核中同时进行来有效地执行包括多个线程的并发程序。这些线程通过同步访问和修改存储在共享内存中的共享资源进行通信。虽然有些问题(创造的并行问题)自然能够利用多核计算,但大多数问题需要巧妙地管理线程同步,这是很难实现的。在多核处理器中,每个处理核心都可以访问一个本地缓冲区,该缓冲区充当一个临时缓存--存储在本地缓冲区中的任何写操作在缓冲区被刷新之前对其他核心不可见。出于效率原因,多核架构实现所谓的松弛内存模型,其中单个线程内的读取和写入事件可能在共享内存中无序地生效,导致程序员可能无法预期的行为。恢复正确性需要在程序代码中手动引入“围栏”指令,这是一项重要的任务-围栏不足会导致不正确的行为,而过度会导致程序效率低下。因此,正如Switt所说,“多核处理器作为标准计算平台的出现将迫使软件设计发生重大变化。“学术界和工业界都在努力更好地利用多核处理,从新的基础和理论基础到开发新的抽象、工具支持、工程范例等。在这个项目中,我们的目标是通过高性能的实用解决方案来简化系统开发。(以提高效率),可验证的正确性(以确保可靠性)和科普松弛内存模型(如现代硬件所使用的)。特别是,我们开发了高效的“并发对象”,提供抽象的低级别的硬件接口和管理线程同步代表程序员。并发对象最终将成为编程语言库的一部分-某些语言,例如,Java已经提供了基本的并发对象作为其标准库的一部分-因此是高度适用的。我们提供的对象将利用宽松的内存模型。这里,众所周知,过于严格的正确性条件(例如,线性化)本身成为效率的障碍。因此,我们开始通过开发新的理论基础的形式放松的正确性条件,匹配宽松的记忆模型。将制定不同条件的层次结构,使人们能够容易地确定每个条件的相对优势。这些条件将被链接到细化的上下文概念,为客户端程序中的可替代性提供基础。这为更有效、可验证正确的并发对象提供了一个基础。我们将专注于开发并发数据结构(例如,堆栈、队列、双端队列)。它们的验证将在KIV定理证明器中机械化,以消除验证中的人为错误,从而提高可靠性。
项目成果
期刊论文数量(10)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
Reducing Opacity to Linearizability: A Sound and Complete Method
将不透明度降低到线性化:一种合理且完整的方法
- DOI:10.48550/arxiv.1610.01004
- 发表时间:2016
- 期刊:
- 影响因子:0
- 作者:Armstrong Alasdair
- 通讯作者:Armstrong Alasdair
Decidability and Complexity for Quiescent Consistency
静态一致性的可判定性和复杂性
- DOI:10.1145/2933575.2933576
- 发表时间:2016
- 期刊:
- 影响因子:0
- 作者:Dongol B
- 通讯作者:Dongol B
Formal Techniques for Distributed Objects, Components, and Systems
分布式对象、组件和系统的形式化技术
- DOI:10.1007/978-3-319-60225-7_8
- 发表时间:2017
- 期刊:
- 影响因子:0
- 作者:Derrick J
- 通讯作者:Derrick J
Formal Techniques for Safety-Critical Systems
安全关键系统的形式化技术
- DOI:10.1007/978-3-319-53946-1_2
- 发表时间:2017
- 期刊:
- 影响因子:0
- 作者:Dongol B
- 通讯作者:Dongol B
Towards linking correctness conditions for concurrent objects and contextual trace refinement
链接并发对象的正确性条件和上下文跟踪细化
- DOI:10.4204/eptcs.209.8
- 发表时间:2016
- 期刊:
- 影响因子:0
- 作者:Dongol B
- 通讯作者:Dongol B
{{
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 }}
Brijesh Dongol其他文献
What Cannot Be Implemented on Weak Memory?
什么不能在弱内存上实现?
- DOI:
- 发表时间:
2024 - 期刊:
- 影响因子:0
- 作者:
Armando Castaneda;Gregory Chockler;Brijesh Dongol;O. Lahav - 通讯作者:
O. Lahav
Deriving real-time action systems in a sampling logic
在采样逻辑中导出实时动作系统
- DOI:
- 发表时间:
2013 - 期刊:
- 影响因子:1.3
- 作者:
Brijesh Dongol;I. Hayes - 通讯作者:
I. Hayes
Progress-based verification and derivation of concurrent programs
基于进度的并发程序验证和推导
- DOI:
- 发表时间:
2009 - 期刊:
- 影响因子:0
- 作者:
Brijesh Dongol - 通讯作者:
Brijesh Dongol
Decidability and complexity for quiescent consistency and its variations
静态一致性及其变化的可判定性和复杂性
- DOI:
- 发表时间:
2015 - 期刊:
- 影响因子:1
- 作者:
Brijesh Dongol;R. Hierons - 通讯作者:
R. Hierons
Enforcing Safety and Progress Properties: An Approach to Concurrent Program Derivation
强化安全性和进度属性:并发程序推导的方法
- DOI:
- 发表时间:
2009 - 期刊:
- 影响因子:0
- 作者:
Brijesh Dongol;I. Hayes - 通讯作者:
I. Hayes
Brijesh Dongol的其他文献
{{
item.title }}
{{ item.translation_title }}
- DOI:
{{ item.doi }} - 发表时间:
{{ item.publish_year }} - 期刊:
- 影响因子:{{ item.factor }}
- 作者:
{{ item.authors }} - 通讯作者:
{{ item.author }}
{{ truncateString('Brijesh Dongol', 18)}}的其他基金
Safe and secure COncurrent programming for adVancEd aRchiTectures (COVERT)
安全可靠的高级架构并发编程 (COVERT)
- 批准号:
EP/X015149/1 - 财政年份:2023
- 资助金额:
$ 12.52万 - 项目类别:
Research Grant
SACRED-MA: Safe And seCure REmote Direct Memory Access
SACRED-MA:安全可靠的远程直接内存访问
- 批准号:
EP/X037142/1 - 财政年份:2023
- 资助金额:
$ 12.52万 - 项目类别:
Research Grant
Verifiably Correct Swarm Attestation
可验证正确的群体证明
- 批准号:
EP/V038915/1 - 财政年份:2021
- 资助金额:
$ 12.52万 - 项目类别:
Research Grant
Verifiably Correct Transactional Memory
可验证正确的事务内存
- 批准号:
EP/R032556/1 - 财政年份:2018
- 资助金额:
$ 12.52万 - 项目类别:
Research Grant
Verifiably correct concurrency abstractions
可验证正确的并发抽象
- 批准号:
EP/R019045/2 - 财政年份:2018
- 资助金额:
$ 12.52万 - 项目类别:
Research Grant
Verifiably correct concurrency abstractions
可验证正确的并发抽象
- 批准号:
EP/R019045/1 - 财政年份:2017
- 资助金额:
$ 12.52万 - 项目类别:
Research Grant
相似海外基金
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
- 资助金额:
$ 12.52万 - 项目类别:
Statistical methods to correct for measurement error in self-reported dietary data from lifestyle intervention trials
纠正生活方式干预试验自我报告饮食数据中测量误差的统计方法
- 批准号:
9292372 - 财政年份:2015
- 资助金额:
$ 12.52万 - 项目类别:
CAREER: Provably Correct Control Software for Autonomous High-Performance Agents
职业生涯:可证明正确的自主高性能代理控制软件
- 批准号:
1351640 - 财政年份:2014
- 资助金额:
$ 12.52万 - 项目类别:
Standard Grant
A METHOD TO CORRECT FOR POPULATION STRUCTURE USING A SEGREGATION MODEL
一种利用隔离模型修正人口结构的方法
- 批准号:
8171730 - 财政年份:2010
- 资助金额:
$ 12.52万 - 项目类别:
A METHOD TO CORRECT FOR POPULATION STRUCTURE USING A SEGREGATION MODEL
一种利用隔离模型修正人口结构的方法
- 批准号:
7956500 - 财政年份:2009
- 资助金额:
$ 12.52万 - 项目类别:
CT-ISG: Implementing Provably Correct High-Performance Ciphers with Sketching
CT-ISG:通过草图实现可证明正确的高性能密码
- 批准号:
0524815 - 财政年份:2005
- 资助金额:
$ 12.52万 - 项目类别:
Standard Grant
CORRECT PAIRING OF INSULIN A AND B CHAINS IN SOLUTION
溶液中胰岛素 A 链和 B 链的正确配对
- 批准号:
3232419 - 财政年份:1984
- 资助金额:
$ 12.52万 - 项目类别:
CORRECT PAIRING OF INSULIN A & B CHAINS IN SOLUTION
胰岛素 A 的正确配对
- 批准号:
3232416 - 财政年份:1984
- 资助金额:
$ 12.52万 - 项目类别: