Advances in 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.