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.