Verification of Hardware Concurrency via Model Learning (CLeVer)

我们的社会越来越依赖于能够同时执行多项任务的数字设备：平板电脑，智能手机，我们的个人电脑，它们都包含能够同时执行多条指令的处理器。这些处理器中的漏洞，比如最近的Meltdown和Spectre，会严重危及用户的安全。随着这些系统复杂性的增加，迫切需要对其正确性进行自动化评估，特别是在与并发相关的方面。形式验证是一种自动检查系统重要属性的高效技术。它依赖于实际系统的一个机器可读的抽象——一个模型。正式验证的一个关键优势是，当模型足够精确时，它能够发现单独使用传统测试很难发现和重现的错误。然而，这些模型通常是由人类构建的，因此容易出错且不准确。此外，复杂的并发行为（如弱内存并发性）使建模更具挑战性。该项目的总体目标是为硬件系统开发一个验证框架，该框架使用人工智能来自动构建和验证更好的模型。最终，这将导致更低的生产成本和更可靠的硬件。这对于设计大规模生产硬件设备的公司（如ARM）尤其重要：设计中的一个错误可能导致数百万个有缺陷的设备被制造出来。这个项目背后的新想法是依靠最初在人工智能中提出的模型学习范式，通过对系统行为的一系列观察，以黑盒方式自动构建运行系统的模型。这种方法在控制复杂性和实现可伸缩性方面非常有效：通过将整个系统或其某些组件视为黑盒，可以微调模型的细节级别，并将分析重点放在特定的特征上。近年来，模型学习已经开始成功地应用于各种学术和工业环境中。然而，使用这种方法开发的模型本质上都是顺序的。硬件系统中并发行为的验证是一个未开发的、具有挑战性的、潜在的有益的应用程序，该项目建议探索。

Our society is increasingly reliant on digital devices that are capable of performing several tasks at the same time: tablets, smartphones, our personal computers, they all contain processors capable of executing multiple instructions concurrently. Bugs in these processors, such as the recent Meltdown and Spectre, can seriously compromise the security and safety of their users. As the complexity of these systems increases, there is a pressing need to automate the assessment of their correctness, especially with respect to concurrency-related aspects.Formal verification is a highly effective technique to automatically check important properties of systems. It relies on a machine-readable abstraction of the actual system---a model. A key strength of formal verification is that, when the model is accurate enough, it is able to find bugs that would be hard to find and reproduce using traditional testing alone. However, these models are usually built by humans and as such can be error-prone and inaccurate. Moreover, sophisticated concurrent behaviours such as weak-memory concurrency make modelling even more challenging.The overall goal of this project is to develop a verification framework for hardware systems that uses artificial intelligence to automatically build and verify better models. Ultimately, this will lead to lower production costs and more reliable hardware.This is particularly important for companies that design hardware units destined to large-scale production, such as ARM: a bug in the design may lead to millions of faulty units being manufactured.The novel idea behind this project is to rely on the model learning paradigm, originally proposed in AI, to automatically build a model of a running system in a black-box fashion---from a series of observations of the behaviour of the system. This approach can be very effective in taming complexity and achieving scalability: by treating the whole system, or some of its components, as black-boxes, one can fine-tune the level of detail of the model and focus the analysis on specific features.In recent years model learning has started to be successfully applied in a variety of academic and industrial contexts. However, the models developed using this approach are all inherently sequential. The verification of concurrent behaviour in hardware systems is an unexplored, challenging, and potentially rewarding application that this project proposes to explore.