Towards Verification of Well-Formed Transactions in Java Card Bytecode

Using transactions in Java Card bytecode programs can be rather tricky and requires special attention from the programmer in order to work around some of the limitations imposed and to avoid introducing serious run-time errors due to inappropriate use of transactions.In this paper we present a novel analysis that combines control and data flow analysis with an analysis that tracks active transactions in a Java Card bytecode program. We formally prove the correctness of the analysis and show how it can be used to solve the above problem of guaranteeing that transactions in a Java Card bytecode program are well-formed and thus do not give rise to run-time errors.     

Precise null-pointer analysis

In Java, C or C++, attempts to dereference the null value result in an exception or a segmentation fault. Hence, it is important to identify those program points where this undesired behaviour might occur or prove the other program points (and possibly the entire program) safe. To that purpose, null-pointer analysis of computer programs checks or infers non-null annotations for variables and object fields. With few notable exceptions, null-pointer analyses currently use run-time checks or are incorrect or only verify manually provided annotations. In this paper, we use abstract interpretation to build and prove correct a first, flow and context-sensitive static null-pointer analysis for Java bytecode (and hence Java) which infers non-null annotations. It is based on Boolean formulas, implemented with binary decision diagrams. For better precision, it identifies instance or static fields that remain always non-null after being initialised. Our experiments show this analysis faster and more precise than the correct null-pointer analysis by Hubert, Jensen and Pichardie. Moreover, our analysis deals with exceptions, which is not the case of most others; its formulation is theoretically clean and its implementation strong and scalable. We subsequently improve that analysis by using local reasoning about fields that are not always non-null, but happen to hold a non-null value when they are accessed. This is a frequent situation, since programmers typically check a field for non-nullness before its access. We conclude with an example of use of our analyses to infer null-pointer annotations which are more precise than those that other inference tools can achieve.     

Automated bug isolation via program chipping

This paper introduces program chipping, a simple yet effective technique to isolate bugs. This technique automatically removes or chips away parts of a program so that the part that contributes to some symptomatic output becomes more apparent to the user. Program chipping is similar in spirit to traditional program slicing and debugging techniques, but chipping uses very simple techniques based on the syntactic structure of the program. We have developed a chipping tool for Java programs, called ChipperJ, and have run it on a variety of small to large programs, including a Java compiler, looking for various symptoms. The results are promising. The reduced program is generally about 20–35% of the size of the original. ChipperJ takes less than an hour on large programs to perform this reduction; even if it took overnight, that would be reasonable if it saves the developer time. Copyright © 2006 John Wiley & Sons, Ltd.     

Dynamic Query-Based Debugging of Object-Oriented Programs

Program errors are hard to find because of the cause-effect gap between the instant when an error occurs and when the error becomes apparent to the programmer. Although debugging techniques such as conditional and data breakpoints help in finding errors in simple cases, they fail to effectively bridge the cause-effect gap in many situations. This paper proposes two debuggers that provide programmers with an instant error alert by continuously checking inter-object relationships while the debugged program is running. We call such tool a dynamic query-based debugger. To speed up dynamic query evaluation, our debugger implemented in portable Java uses a combination of program instrumentation, load-time code generation, query optimization, and incremental reevaluation. Experiments and a query cost model show that selection queries are efficient in most cases, while more costly join queries are practical when query evaluations are infrequent or query domains are small. To enable query-based debugging in the middle of program execution in a portable way, our debugger performs efficient Java class file instrumentation. We call such debugger an on-the-fly debugger. Though the on-the-fly debugger has a higher overhead than a dynamic query-based debugger, it offers additional interactive power and flexibility while maintaining complete portability.     

Compact visualization of Java program execution

The context of this work is a practical, open‐source visualization system, called JIVE, that supports two forms of runtime visualizations of Java programs – object diagrams and sequence diagrams. They capture, respectively, the current execution state and execution history of a Java program. These diagrams are similar to those found in the UML for specifying design–time decisions. In our work, we construct these diagrams at execution time, thereby ensuring continuity of notation from design to execution. In so doing, a few extensions to the UML notation are proposed in order to better represent runtime behavior. As sequence diagrams can become long and unwieldy, we present techniques for their compact representation. A key result in this paper is a novel labeling scheme based upon regular expressions to compactly represent long sequences and an O(r²) algorithm for computing these labels, where r is the length of the input sequence, based upon the concept of ‘tandem repeats’ in a sequence. Horizontal compaction greatly helps minimize the extent of white space in sequence diagrams by the elimination of object lifelines and also by grouping lifelines together. We propose a novel extension to the sequence diagram to deal with out‐of‐model calls when the lifelines of certain classes of objects are filtered out of the visualization, but method calls may occur between in‐model and out‐of‐model calls. The paper also presents compaction techniques for multi‐threaded Java execution with different forms of synchronization. Finally, we present experimental results from compacting the runtime visualizations of a variety of Java programs and execution trace sizes in order to demonstrate the practicality and efficacy of our techniques. Copyright © 2016 John Wiley & Sons, Ltd.     

一种基于类的Java多线程程序数据竞争静态检测算法

多线程并发程序的广泛使用引发了更多的数据竞争问题,竞争检测对于提高软件质量具有重要意义。将竞争静态检测和静态切片分析结合起来,提出了一种基于类的Java数据竞争静态检测算法,该算法利用函数调用层次获得函数调用链,对类域进行分析,找出可能数据竞争,通过静态切片缩小程序分析范围,并结合数据竞争的必要条件,去掉不可能数据竞争。实例表明,该算法可用于指导修复程序中的竞争缺陷。     

一种Java并发程序死锁动态检测的新方法

死锁是并发程序中最为常见的一类错误,直到现在并没有得到很好地解决.本文以Java并发程序为例,重点研究针对资源死锁较为有效的动态检测算法:根据并发程序的动态执行追踪信息,分析出加锁控制依赖关系,再根据死锁所应满足的条件在该依赖关系集上作适量演算便得到潜在死锁关系对.进一步地,结合线程间控制流图所反映的部分静态依赖关系,剔除假性死锁关系对,提高了计算结果的精度.该算法显著的特点是简单易于实现,且无需构造锁树或锁图等图形表示.     

A Java extension with support for dimensions

We present an extension to the Java language with support for physical dimensions and units of measurement. This should reduce programming errors in scientific and technological areas. We discuss various aspects of dimensions and units, and then design principles for support in programming languages. An overview of earlier work shows that some language extensions focused on units, whereas we argue that dimensions are a better starting point; units can then simply be treated as constants. Then we present the Java extension, and show how to define and use dimensions and units. The communication between the program and the outer world gets special attention. The programmer can still make dimensional errors there, but we claim the risk is reduced. It has been simple to build support for this extension into an existing Java compiler. We outline the applied technique. Copyright © 1999 John Wiley & Sons, Ltd.     

Towards Language-Agnostic Mobile Code

The Java Virtual Machine is primarily designed for transporting Java programs. As a consequence, when JVM bytecodes are used to transport programs in other languages, the result becomes less acceptable the more the source language diverges from Java. Microsoft's .NET transport format fares better in this respect because it has a more flexible type system and instruction set, but it is not extensible, and (for example) has no provision for supporting explicit programmer-specified parallelism. Both platforms have difficulty making transported programs run efficiently.This paper discusses first steps towards mobile code representations that are independent (in the sense that the representation can be appropriately parameterized) of the source language (e.g., Java), intermediate representation (e.g., bytecode), and target architecture (e.g., x86). We call this kind of parameterizable framework language-agnostic.We present two techniques which provide parts of the envisioned language-agnostic functionality. Compressed abstract syntax trees as a wire format provide for a very dense encoding of programs at a high level of abstraction. We show how to parameterize the compression algorithm in a modular fashion with knowledge beyond the purely syntactical level. This leads to the notion of well-formedness by construction. The second technique defines the semantics of programs by mapping from abstract syntax trees to a typed core calculus representation. Based on this representation it becomes possible to use portable definitions of security policies and to execute programs written in different source languages, even if a more efficient trusted native compiler is not available on the target platform.     

Estimation of dynamical characteristics of a parallel program on a model

This paper considers a model of a parallel program that can efficiently be interpreted on an instrumental computer, providing a means for a sufficiently accurate prediction of the actual time needed for execution of the parallel program on a given parallel computational system. The model is designed for parallel programs with explicit message passing written in Java with calls to the MPI library and is a part of the ParJava environment. The model is obtained by transforming the program control tree, which, for Java programs, can be constructed by modifying the abstract syntax tree. The communication functions are simulated on the basis of the LogGP model, which makes it possible to take into account specific features of the distributed computational system.     

Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java

This paper shows how to integrate two complementary techniques for manipulating program invariants: dynamic detection and static verification. Dynamic detection proposes likely invariants based on program executions, but the resulting properties are not guaranteed to be true over all possible executions. Static verification checks that properties are always true, but it can be difficult and tedious to select a goal and to annotate programs for input to a static checker. Combining these techniques overcomes the weaknesses of each: dynamically detected invariants can annotate a program or provide goals for static verification, and static verification can confirm properties proposed by a dynamic tool.We have integrated a tool for dynamically detecting likely program invariants, Daikon, with a tool for statically verifying program properties, ESC/Java. Daikon examines run-time values of program variables; it looks for patterns and relationships in those values, and it reports properties that are never falsified during test runs and that satisfy certain other conditions, such as being statistically justified. ESC/Java takes as input a Java program annotated with preconditions, postconditions, and other assertions, and it reports which annotations cannot be statically verified and also warns of potential runtime errors, such as null dereferences and out-of-bounds array indices.Our prototype system runs Daikon, inserts its output into code as ESC/Java annotations, and then runs ESC/Java, which reports unverifiable annotations. The entire process is completely automatic, though users may provide guidance in order to improve results if desired. In preliminary experiments, ESC/Java verified all or most of the invariants proposed by Daikon.     

A decision procedure for detecting atomicity violations for communicating processes with locks

The problem of interest is to verify data consistency of a concurrent Java program. In particular, we present a new decision procedure for verifying that a class of data races caused by inconsistent accesses on multiple fields of an object cannot occur (so-called atomic-set serializability). Atomic-set serializability generalizes the ordinary notion of a data race (i.e., inconsistent coordination of accesses on a single memory location) to a broader class of races that involve accesses on multiple memory locations. Previous work by some of the authors presented a technique to abstract a concurrent Java program into an EML program, a modeling language based on pushdown systems and a finite set of reentrant locks. Our previous work used only a semi-decision procedure, and hence provides a definite answer only some of the time. In this paper, we rectify this shortcoming by developing a decision procedure for verifying data consistency, i.e., atomic-set serializability, of an EML program. When coupled with the previous work, it provides a decision procedure for verifying data consistency of a concurrent Java program. We implemented the decision procedure, and applied it to detect both single-location and multi-location data races in models of concurrent Java programs. Compared with the prior method based on a semi-decision procedure, not only was the decision procedure 34 times faster overall, but the semi-decision procedure timed out on about 50% of the queries, whereas the decision procedure timed out on none of the queries.     

Middleware infrastructure for parallel and distributed programming models in heterogeneous systems

We introduce a middleware infrastructure that provides software services for developing and deploying high-performance parallel programming models and distributed applications on clusters and networked heterogeneous systems. This middleware infrastructure utilizes distributed agents residing on the participating machines and communicating with one another to perform the required functions. An intensive study of the parallel programming models in Java has helped identify the common requirements for a runtime support environment, which we used to define the middleware functionality. A Java-based prototype, based on this architecture, has been developed along with a Java object-passing interface (JOPI) class library. Since this system is written completely in Java, it is portable and allows executing programs in parallel across multiple heterogeneous platforms. With the middleware infrastructure, users need not deal with the mechanisms of deploying and loading user classes on the heterogeneous system. Moreover, details of scheduling, controlling, monitoring, and executing user jobs are hidden, while the management of system resources is made transparent to the user. Such uniform services are essential for facilitating the development and deployment of scalable high-performance Java applications on clusters and heterogeneous systems. An initial deployment of a parallel Java programming model over a heterogeneous, distributed system shows good performance results. In addition, a framework for the agents' startup mechanism and organization is introduced to provide scalable deployment and communication among the agents.     

Improving the Decompilation of Java Bytecode to Prolog by Partial Evaluation

The interpretative approach to compilation allows compiling programs by partially evaluating an interpreter w.r.t. a source program. This approach, though very attractive in principle, has not been widely applied in practice mainly because of the difficulty in finding a partial evaluation strategy which always obtain “quality” compiled programs. In spite of this, in recent work we have performed a proof of concept of that, at least for some examples, this approach can be applied to decompile Java bytecode into Prolog. This allows applying existing advanced tools for analysis of logic programs in order to verify Java bytecode. However, successful partial evaluation of an interpreter for (a realistic subset of) Java bytecode is a rather challenging problem. The aim of this work is to improve the performance of the decompilation process above in two respects. First, we would like to obtain quality decompiled programs, i.e., simple and small. We refer to this as the effectiveness of the decompilation. Second, we would like the decompilation process to be as efficient as possible, both in terms of time and memory usage, in order to scale up in practice. We refer to this as the efficiency of the decompilation. With this aim, we propose several techniques for improving the partial evaluation strategy. We argue that our experimental results show that we are able to improve significantly the efficiency and effectiveness of the decompilation process.     

Statically safe program generation with SafeGen

SafeGen is a meta-programming language for writing statically safe generators of Java programs. If a program generator written in SafeGen passes the checks of the SafeGen compiler, then the generator will only generate well-formed Java programs, for any generator input. In other words, statically checking the generator guarantees the correctness of any generated program, with respect to static checks commonly performed by a conventional compiler (including type safety, existence of a superclass, etc.). To achieve this guarantee, SafeGen supports only language primitives for reflection over an existing well-formed Java program, primitives for creating program fragments, and a restricted set of constructs for iteration, conditional actions, and name generation. SafeGen’s static checking algorithm is a combination of traditional type checking for Java, and a series of calls to a theorem prover to check the validity of first-order logical sentences, constructed to represent well-formedness properties of the generated program under all inputs. The approach has worked quite well in our tests, providing proofs for correct generators or pointing out interesting bugs.     

ContainerCloudSim: An environment for modeling and simulation of containers in cloud data centers

Containers are increasingly gaining popularity and becoming one of the major deployment models in cloud environments. To evaluate the performance of scheduling and allocation policies in containerized cloud data centers, there is a need for evaluation environments that support scalable and repeatable experiments. Simulation techniques provide repeatable and controllable environments, and hence, they serve as a powerful tool for such purpose. This paper introduces ContainerCloudSim, which provides support for modeling and simulation of containerized cloud computing environments. We developed a simulation architecture for containerized clouds and implemented it as an extension of CloudSim. We described a number of use cases to demonstrate how one can plug in and compare their container scheduling and provisioning policies in terms of energy efficiency and SLA compliance. Our system is highly scalable as it supports simulation of large number of containers, given that there are more containers than virtual machines in a data center. Copyright © 2016 John Wiley & Sons, Ltd.     

An update calculus for expressing type-safe program updates

The dominant share of software development costs is spent on software maintenance, particularly the process of updating programs in response to changing requirements. Currently, such program changes tend to be performed using text editors, an unreliable method that often causes many errors. In addition to syntax and type errors, logical errors can be easily introduced since text editors cannot guarantee that changes are performed consistently over the whole program. All these errors can cause a correct and perfectly running program to become instantly unusable. It is not surprising that this situation exists because the “text-editor method” reveals a low-level view of programs that fails to reflect the structure of programs.We address this problem by pursuing a programming-language-based approach to program updates. To this end we discuss in this paper the design and requirements of an update language for expressing update programs. We identify as the essential part of any update language a scope update that performs coordinated update of the definition and all uses of a symbol. As the underlying basis for update languages, we define an update calculus for updating lambda calculus programs. We develop a type system for the update calculus that infers the possible type changes that can be caused by an update program. We demonstrate that type-safe update programs that fulfill certain structural constraints preserve the type correctness of lambda terms. The update calculus can serve as a basis for higher-level update languages, such as for Haskell or Java.     

Space efficient execution of deterministic parallel programs

We model a deterministic parallel program by a directed acyclic graph of tasks, where a task can execute as soon as all tasks preceding it have been executed. Each task can allocate or release an arbitrary amount of memory (i.e., heap memory allocation can be modeled). We call a parallel schedule “space efficient” if the amount of memory required is at most equal to the number of processors times the amount of memory required for some depth-first execution of the program by a single processor. We describe a simple, locally depth-first scheduling algorithm and show that it is always space efficient. Since the scheduling algorithm is greedy, it will be within a factor of two of being optimal with respect to time. For the special case of a program having a series-parallel structure, we show how to efficiently compute the worst case memory requirements over all possible depth-first executions of a program. Finally, we show how scheduling can be decentralized, making the approach scalable to a large number of processors when there is sufficient parallelism     

示例演化驱动的学生程序自动修复

已有的程序自动化调试研究大多面向工业软件,而学生程序调试具有缺陷数多、类型复杂等特有难点问题,因此,针对学生程序设计应用背景,研究程序自动修复方法,利用模板示例程序指导补丁的演化.改进了遗传编程算法,包括适应度的计算、变异体的生成方式和变异位置及操作的选择方式,使其更加适合修复学生程序.提出了基于示例的静态错误定位方法,能够识别缺陷程序和参考程序差异和可能的变异操作,有效地缩小补丁的搜索空间以提高修复的准确性.提出了基于执行值序列的变量映射方法,以降低变异体的编译错误,提高修复的准确性.在此基础上,设计并实现了示例演化驱动的Java学生程序自动修复系统.实验结果表明,该方法可以修复含有多缺陷学生程序,对于所用的测试集,当学生程序只有1个~2个错误时,修复率将近100%;当含有3个缺陷时,修复率约为70%;当含有4个及以上缺陷时,修复率约为50%.     

Symbolic execution with abstraction

We address the problem of error detection for programs that take recursive data structures and arrays as input. Previously we proposed a combination of symbolic execution and model checking for the analysis of such programs: we put a bound on the size of the program inputs and/or the search depth of the model checker to limit the search state space. Here we look beyond bounded model checking and consider state matching techniques to limit the state space. We describe a method for examining whether a symbolic state that arises during symbolic execution is subsumed by another symbolic state. Since the number of symbolic states may be infinite, subsumption is not enough to ensure termination. Therefore, we also consider abstraction techniques for computing and storing abstract states during symbolic execution. Subsumption checking determines whether an abstract state is being revisited, in which case the model checker backtracks—this enables analysis of an under-approximation of the program behaviors. We illustrate the technique with abstractions for lists and arrays. We also discuss abstractions for more general data structures. The abstractions encode both the shape of the program heap and the constraints on numeric data. We have implemented the techniques in the Java PathFinder tool and we show their effectiveness on Java programs. This paper is an extended version of Anand et al. (Proceedings of SPIN, pp. 163–181, 2006).