Advances in Program Analysis

拟议的研究是在程序分析领域，这是自动分析计算机程序的行为的过程。程序分析在软件验证领域有着广泛的应用，其目的是使用自动化技术和工具来确保软件的可靠性。随着软件在我们生活的各个方面无处不在，确保软件的可靠性变得至关重要。 随着多核处理器成为计算机和移动的设备的默认选择以及分布式Web服务的出现，并发性在应用软件中已经变得司空见惯。由于并发执行程序线程之间的不确定性交互，并发程序的设计是出了名的容易出错。本文的研究将推动并发软件分析的发展。更具体地说，我们将专注于实现这一点，在一些最广泛使用的编程语言的功能，结合并发性，使程序分析的任务变得困难，因此缺乏有效的程序分析技术。在过去的几年里，我们已经取得了重大进展，引入了一种新的方法来处理这个问题域，基于的概念，并计划释放他们的力量来解决并发研究中一些最具挑战性的问题，包括： 无限并发：当对构成程序的交互进程的数量没有先验限制时，程序分析变得相当复杂。这通常被称为无限并发。许多广泛使用的软件系统，例如设备驱动程序，文件系统和并发库自然地遵循这个模型，这使得它们的验证问题非常相关。 动态内存（堆）：所有现代编程语言都有动态创建和操作内存的原语，现在几乎不可能找到不使用动态内存的软件。关于程序操纵堆的推理是一个理论上和实践上都很困难的问题，即使没有并发的存在，特别是更具有挑战性。挑战通常是对堆有足够精确的理解，而不会妨碍程序分析的任务。 宽松的内存一致性：并发程序在不同的内存模型下有不同的行为，保证不同级别的内存一致性。在顺序一致性内存模型中，执行中有一个单一的全局时间视图。在松弛内存模型中，每个处理器都有自己的时间视图，并且视图可能不一致。由于没有实际的计算机实现顺序一致性内存模型，在宽松的内存模型（一项具有挑战性的任务）下分析程序是获得实际相关结果的唯一可能方法。 数值不确定性：科学应用，如高通量医学成像或气候模型的高性能模拟，需要大量的计算资源。这些科学应用程序通常在多核和多处理器环境中运行。问题是，同一个并发程序在使用不同的架构和编译器时可能会产生不同的结果，这种敏感性对于浮点计算来说尤其重要。这是由于浮点行为对执行顺序（由并发执行模型确定）的一些众所周知的和一些不太为人所知的依赖性。这使得跨平台计算结果的可移植性和可靠性受到质疑，这使得这一未充分探索的问题领域值得关注。

The proposed research is in the area of Program Analysis, which is the process of automatically analyzing the behaviour of computer programs. A well-stablished application of program analysis has been in the domain of Software Verification which aims at ensuring the reliability of software, using automated techniques and tools. With the emerging omnipresence of software in all aspects of our lives, ensuring reliability of software has become essential. With multicore processors becoming the default choice for computers and mobile devices and the advent of distributed web services, concurrency has become commonplace in application software. The design of concurrent programs is notoriously error-prone due to the nondeterministic interactions among concurrently executing program threads. The proposed research will advance the state of the art in concurrent software analysis. More specifically, we will focus on achieving this in the presence of some the most widely used programming language features that, combined with concurrency, make the task of program analysis difficult and consequently there is a shortage of effective program analysis techniques. We have made significant progress in the past few years by introducing a novel way of approaching this problem domain, based on the notion of dataflow, and plan to unleash their power for addressing some of the most challenging problems in concurrency research, including: Unbounded Concurrency: program analysis becomes substantially more complicated when there is no a priori bound on the number of interacting processes that constitute a program. This is usually referred to as unbounded concurrency. Many broadly used software systems, for example device drivers, file systems, and concurrent libraries naturally adhere to this model, which makes their verification problem very relevant. Dynamic Memory (heap): All modern programming languages have primitives for creating and manipulating memory dynamically, and it is virtually impossible nowadays to find software that does not use dynamic memory. Reasoning about programs manipulating the heap, which is unbounded, is a theoretically and practically hard problem, even without the presence of concurrency, and particularly more challenging with it. The challenge is usually in producing a precise enough understanding of the heap that will not hinder the task of program analysis. Relaxed Memory Consistency: Concurrent programs have different behaviours under different memory models guaranteeing different levels of memory consistency. In the sequential consistency memory model, there is a single, global view of time in an execution. In relaxed memory models, each processor has its own view of time, and the views may not be consistent. Since no actual computer implements sequential consistency memory model, analyzing programs under a relaxed memory model (a challenging task) is the only possible way of getting practically relevant results. Numerical Uncertainty : Scientific applications, like high-throughput medical imaging or high-performance simulations of climate models, demand great computational resources. These scientific applications are typically run on multicore and multi-processor environments. The problem is that the same concurrent program can produce different results when used with different architectures and compilers, a sensitivity that is especially critical for floating-point computations. These are due to some well-known and some lesser- known dependencies of floating-point behaviour on execution order (which is determined by the concurrent execution model). This puts the portability and reliability of computation results across platforms under question, which makes this under-explored problem area worthy of attention.