权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Verifying Concurrent Lock-free Algorithms

验证并发无锁算法

基本信息

批准号：
EP/J003727/1
负责人：
John Derrick
金额：
$ 48.28万
依托单位：
University of Sheffield
依托单位国家：
英国
项目类别：
Research Grant
财政年份：
2012
资助国家：
英国
起止时间：
2012 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=EP%2FJ003727%2F1
关键词：
Verifying Concurrent Lock free Algorithms

项目摘要

Software is becoming increasingly complex, and the demand for increased performance is driven by many diverse applications. As a response to this demand, concurrent software that efficiently exploits multi-core architectures is likely to be the norm in many sectors. However, developing correct concurrent algorithms is a difficult task. This is particularly true for a class of concurrent algorithms that fully exploit the potential concurrency by offering the maximum amount of interleavings of different processes working on a shared memory. There is then a real economic imperative to build techniques that can verify as correct such lock-free algorithms as they are known.Testing and simulation, while valuable and automated to a degree, are ultimately limited in the guarantees they can offer for correctness, particularly in the case of concurrent algorithms, where multiple thread interleavings act on data structures potentially unbounded in size. Formal verification of this class of algorithm is becoming tractable and there has been a surge of interest in applying such techniques, and a unique opportunity to verify a class of algorithms before their widespread adoption.This project focusses on lock-free algorithms (also called non-blocking algorithms). Lock-free algorithms have been discovered for many common data structures. Non-blocking algorithms are used extensively at the operating system and JVM level for tasks such as thread and process scheduling. While they are more complicated to implement, they have a number of advantages over lock-based alternatives -- hazards like priority inversion and deadlock are avoided, contention is less expensive, and coordination occurs at a finer level of granularity, enabling a higher degree of parallelism.This project seeks to develop techniques whereby such algorithms can be proved correct. The techniques are based on the notion of refinement which relates an abstract specification with a more detailed concrete implementation. What we will do here is show that a certain type of refinement between an abstract description and a concurrent algorithm implies that the concurrent algorithm is correct. The notion of correctness here being linearizability.Part of the novelty of what we propose to do is in the construction of the right sort of refinement relation - it has to be one that will imply linearizability, yet at the same time give rise to proof obligations that are tractable for specific algorithms, that is, actually make the verification of linearizability easier to achieve. Another part of the novelty is that we will mechanize the whole thing - both the proofs for specific algorithms, but also the proof that our technique is correct, thus giving an extra level of assurance that the techniques really are sound - the details are sufficiently complex and subtle that mechanization really is necessary to be 100% sure of correctness.In addition to these basics we want a proof method that is applicable to a wide range of algorithms, and one that is compositional. To aid applicability we develop two flavours of technique - one based on forward simulation, and another based on backward simulation, as well as specific support for unboundedness and dynamic linearization points. To aid compositionality (so that the proofs can be broken down into smaller local steps rather than undertaking one large global proof) we will develop thread modular simulation conditions, and interference freedom conditions that aid the process.Our work will be evaluated on a number of 'benchmark' algorithms, such as lock-free implementations of stacks, queues, hashtables etc. Finally, we will investigate how our proof methods can be shown to be complete, that is, every algorithm could potentially be verified by using the method. We will also investigate liveness, ie, showing that a concurrent algorithm guarantees various forms of progression.

软件正变得越来越复杂，许多不同的应用程序驱动着对提高性能的需求。作为对这一需求的响应，有效利用多核架构的并发软件很可能成为许多领域的标准。然而，开发正确的并发算法是一项艰巨的任务。对于一类并发算法来说尤其如此，这些算法通过提供在共享内存上工作的不同进程的最大数量的交叉来充分利用潜在的并发性。因此，构建能够验证这种无锁算法是否正确的技术是一种真正的经济需要。测试和模拟虽然在一定程度上是有价值的和自动化的，但它们最终在保证正确性方面受到限制，特别是在并发算法的情况下，其中多个线程交织作用于可能无限大小的数据结构。这类算法的正式验证正在变得容易处理，并且对应用此类技术的兴趣激增，并且在广泛采用之前验证一类算法的独特机会。该项目关注无锁算法（也称为非阻塞算法）。对于许多常见的数据结构，已经发现了无锁算法。非阻塞算法在操作系统和JVM级别广泛用于线程和进程调度等任务。虽然它们的实现更复杂，但与基于锁的替代方案相比，它们有许多优点——避免了优先级反转和死锁等危险，争用成本更低，协调发生在更细的粒度级别，从而实现了更高程度的并行性。该项目旨在开发技术，从而证明这些算法是正确的。这些技术基于细化的概念，将抽象规范与更详细的具体实现联系起来。我们在这里要做的是展示抽象描述和并发算法之间的某种细化意味着并发算法是正确的。正确性的概念是线性化。我们建议做的部分新颖之处在于构建正确的细化关系——它必须是一个暗示线性化的关系，但同时又产生了对特定算法易于处理的证明义务，也就是说，实际上使线性化的验证更容易实现。另一个新奇之处在于，我们将把整个事情机械化——既包括对特定算法的证明，也包括对我们技术正确性的证明，从而为技术确实是合理的提供了额外的保证——细节足够复杂和微妙，机械化对于100%确保正确性是必要的。除了这些基础之外，我们还需要一种适用于各种算法的证明方法，并且是复合的。为了帮助应用，我们开发了两种风格的技术-一种基于前向模拟，另一种基于后向模拟，以及对无界性和动态线性化点的特定支持。为了帮助组合性（这样证明可以被分解成更小的局部步骤，而不是进行一个大的全局证明），我们将开发线程模块化仿真条件，以及帮助该过程的干扰自由条件。我们的工作将在许多“基准”算法上进行评估，例如堆栈、队列、哈希表等的无锁实现。最后，我们将研究如何证明我们的证明方法是完整的，也就是说，每个算法都可以通过使用该方法进行验证。我们还将研究活动性，即显示并发算法保证各种形式的进展。