Advances in Program Analysis

程序分析的进展

• 批准号: RGPIN-2014-04450
• 负责人: Farzan, Azadeh
• 金额: $ 2.84万
• 依托单位: University of Toronto
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2014
• 资助国家: 加拿大
• 起止时间: 2014-01-01 至 2015-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=566529
• 关键词: Advances; Program; Analysis

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.

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