http://labs.oracle.com/rss/publications.php Updated Tue, 08 Nov 2011 20:48:00 -0800 en Tue, 08 Nov 2011 20:48:00 -0800 Wed, 16 May 2012 04:11:37 -0700 http://labs.oracle.com/admin/images/ocom/hp/oralogo_small.gif http://labs.oracle.com/rss/publications.php 133 18 Oracle Logo http://dx.doi.org/10.1016/j.future.2010.11.006 http://dx.doi.org/10.1016/j.future.2010.11.006 Sun, 01 Jan 2012 08:33:00 -0800 http://doi.ieeecomputersociety.org/10.1109/TPDS.2011.140 http://doi.ieeecomputersociety.org/10.1109/TPDS.2011.140 Sun, 01 Jan 2012 09:03:00 -0800 http://dx.doi.org/10.1016/j.ins.2011.10.004 http://dx.doi.org/10.1016/j.ins.2011.10.004 Sun, 01 Jan 2012 14:48:00 -0800 http://dx.doi.org/10.1016/j.jvcir.2011.09.001 http://dx.doi.org/10.1016/j.jvcir.2011.09.001 Sun, 01 Jan 2012 04:56:00 -0800 http://dx.doi.org/10.1016/j.neucom.2011.09.007 http://dx.doi.org/10.1016/j.neucom.2011.09.007 Sun, 01 Jan 2012 06:46:00 -0800 http://dx.doi.org/10.1016/j.cviu.2011.10.007 http://dx.doi.org/10.1016/j.cviu.2011.10.007 Sun, 01 Jan 2012 10:11:00 -0800 http://labs.oracle.com/docs/index.php?id=2011-0332 http://labs.oracle.com/docs/index.php?id=2011-0332 Slides for talk at WTTM 2011 Tue, 08 Nov 2011 10:42:00 -0800 http://labs.oracle.com/docs/index.php?id=2011-0306 http://labs.oracle.com/docs/index.php?id=2011-0306 This is a translation from Russian of the paper for the conference "Statistics, Simulation, Optimization - 2011" to be held in Chelyabinsk, Russia. The JInterval library is an interval arithmetic library for Java. It was developed in collaboration with the Altai University, Barnaul, Russia. This paper presents the key architectural decisions made when designing JInterval library. It discusses compliance with functional requirements of the library as well as the current status of JInterval. Mon, 17 Oct 2011 13:35:00 -0700 http://labs.oracle.com/docs/index.php?id=2011-0274 http://labs.oracle.com/docs/index.php?id=2011-0274 Over the last decade, great progress has been made in developing practical transactional memory (TM) implementations, but relatively little attention has been paid to precisely specifying what it means for them to be correct, or formally proving that they are. In this paper, we present TMS1 (Transactional Memory Specification 1), a precise specification of correct behaviour of a TM runtime library. TMS1 targets TM runtimes used to implement transactional features in an unmanaged programming language such as C or C++. In such contexts, even transactions that ultimately abort must observe consistent states of memory; otherwise, unrecoverable errors such as divide-by-zero may occur before a transaction aborts, even in a correct program in which the error would not be possible if transactions were executed atomically. We specify TMS1 precisely using an I/O automaton (IOA). This approach enables us to also model TM implementations using IOAs and to construct fully formal and machine-checked correctness proofs for them using well established proof techniques and tools. We outline key requirements for a TM system. To avoid precluding any implementation that satisfies these requirements, we specify TMS1 to be as general as we can, consistent with these requirements. The cost of such generality is that the condition does not map closely to intuition about common TM implementation techniques, and thus it is difficult to prove that such implementations satisfy the condition. To address this concern, we present TMS2, a more restrictive condition that more closely reflects intuition about common TM implementation techniques. We present a simulation proof that TMS2 implements TMS1, thus showing that to prove that an implementation satisfies TMS1, it suffices to prove that it satisfies TMS2. We have formalised and verified this proof using the PVS specification and verification system. Wed, 28 Sep 2011 08:43:00 -0700 http://labs.oracle.com/docs/index.php?id=2011-0246 http://labs.oracle.com/docs/index.php?id=2011-0246 Slides of our paper "Boosting the performance of flow-sensitive points-to analysis using Value Flow" (archivist id 2011-0189), to present at the joint conference of European Software Engineering Conference and the ACM SigSoft Symposium on the Foundation of Software Engineering 2011 (ESEC-FSE'11). The main conference is held at Szeged, Hungry from 5/Sep to 9/Sep, details can be found in the conference website http://2011.esec-fse.org/. This presentation is scheduled on 9/Sep. Thu, 01 Sep 2011 16:46:00 -0700 http://labs.oracle.com/docs/index.php?id=2011-0248 http://labs.oracle.com/docs/index.php?id=2011-0248 Slides of our tool demo "Static Deep Error Checking in Large System Applications Using Parfait " (archivist id 2011-0190), to present at the joint conference of European Software Engineering Conference and the ACM SigSoft Symposium on the Foundation of Software Engineering 2011 (ESEC-FSE'11). The main conference is held at Szeged, Hungry from 5/Sep to 9/Sep, details can be found in the conference website http://2011.esec-fse.org/. This demo and presentation is scheduled on 8/Sep. Thu, 01 Sep 2011 08:14:00 -0700 http://labs.oracle.com/docs/index.php?id=2011-0218 http://labs.oracle.com/docs/index.php?id=2011-0218 This paper is a submission to the IEEE Radio Frequency Integration Technology (RFIT) conference, http://www.ieee-rfit.org. This is an invited submission to be presented at a special session on "Wireless Replacement of Wireline I/O." Conference Date: Nov 30 - Dec 2, 2011; Location: Beijing, China. Thu, 11 Aug 2011 14:15:00 -0700 http://labs.oracle.com/docs/index.php?id=2011-0208 http://labs.oracle.com/docs/index.php?id=2011-0208 The talk gives an overview of the development of a family of Smalltalk virtual machine implementations called SOM (Simple Object Machine). The SOM VM, originating from the University of Aarhus, Denmark, has been ported to several programming languages, exploring different objectives. All of the VM implementations focus on providing an easily accessible workbench for teaching, but have also turned out to be a viable research platform. In this talk, each of the SOM VMs will be briefly described along with the results that were achieved in applying it in teaching at both undergraduate and graduate levels as well as research. Wed, 03 Aug 2011 22:27:00 -0700 http://labs.oracle.com/docs/index.php?id=2011-0189 http://labs.oracle.com/docs/index.php?id=2011-0189 Points-to analysis is a fundamental static analysis technique which computes the set of memory objects that a pointer may point to. Many different applications, such as security-related program analyses, bug checking, and analyses of multi-threaded programs, require precise points-to information to be effective. Recent work has focused on improving the precision of points-to analysis through \emph{flow-sensitivity} and great progress has been made. However, even with all recent progress, flow-sensitive points-to analysis can still be much slower than a flow-insensitive analysis. In this paper, we propose a novel method that simplifies flow-sensitive points-to analysis to a general graph reachability problem in a value flow graph. The value flow graph summarizes dependencies between pointer variables, including those memory dependencies via pointer dereferences. The points-to set for each pointer variable can then be computed as the set of memory objects that can reach it in the graph. We develop an algorithm to build the value flow graph efficiently by examining the \emph{pointed-to-by} set of a memory object, i.e., the set of pointers that point to an object. The pointed-to-by information of memory objects is very useful for applications such as escape analysis, and information flow analysis. Our approach is intuitive, easy to implement and very efficient. The implementation is around 2000 lines of code and it is more efficient than existing flow-sensitive points-to analyses. The runtime is comparable with the state-of-the-art flow-insensitive points-to analysis. Mon, 04 Jul 2011 12:37:00 -0700 http://labs.oracle.com/docs/index.php?id=2011-0190 http://labs.oracle.com/docs/index.php?id=2011-0190 In this paper, we introduce Parfait, a static bug-checking tool for C/C++ applications. Parfait achieves precision and scalability at the same time by employing a layered program analysis framework. In Parfait, different analyses varying in precision and runtime expense can be invoked on demand to detect defects of a specific type, effectively achieving higher precision with smaller runtime overheads. Several production organizations within Oracle have started to integrate Parfait into their development process. Feedback from various production teams suggests that it is precise and scalable: the tool is able to analyze the OpenSolaris\texttrademark\ operating system and network consolidation (ON) with more than 6 million lines of code in 1 hour, and report thousands of defects with a false positive rate of close to 10\%. Mon, 04 Jul 2011 05:22:00 -0700