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.