Semantics and Algebraic Specification
Essays Dedicated to Peter D. Mosses on the Occasion of His 60th Birthday
Page
%P
-
Chapter and Conference Paper
Automatic Atomicity Verification for Clients of Concurrent Data Structures
Mainstream programming languages offer libraries of concurrent data structures. Each method call on a concurrent data structure appears to take effect atomically. However, clients of such data structures often...
-
Chapter and Conference Paper
Decomposing Opacity
Transactional memory (TM) algorithms are subtle and the TM correctness conditions are intricate. Decomposition of the correctness condition can bring modularity to TM algorithm design and verification. We pres...
-
Chapter and Conference Paper
Proving Non-opacity
Guerraoui and Kapalka defined opacity as a safety criterion for transactional memory algorithms in 2008. Researchers have shown how to prove opacity, while little is known about pitfalls that can lead to non-o...
-
Chapter
Overloading Is NP-Complete
We show that overloading is NP-complete. This solves exercise 6.25 in the 1986 version of the Dragon book.
-
Chapter and Conference Paper
Efficient May Happen in Parallel Analysis for Async-Finish Parallelism
For concurrent and parallel languages, the may-happen-in-parallel (MHP) decision problem asks, given two actions in the program, if there is an execution in which they can execute in parallel. Closely related,...
-
Chapter and Conference Paper
Punctual Coalescing
Compilers use register coalescing to avoid generating code for copy instructions. For architectures with register aliasing such as x86, Smith, Ramsey, and Holloway (2004) presented a polynomial-time approach, ...
-
Book
-
Book and Conference Proceedings
Static Analysis
16th International Symposium, SAS 2009, Los Angeles, CA, USA, August 9-11, 2009. Proceedings
-
Chapter
Tribute to Peter Mosses
We offer this festschrift in tribute to Peter and in celebration of his 60th birthday. An academic symposium marked this event on September 10, 2009.
-
Chapter
Vertical Object Layout and Compression for Fixed Heaps
Research into embedded sensor networks has placed increased focus on the problem of develo** reliable and flexible software for microcontroller-class devices. Languages such as nesC [10] and Virgil [20] have...
-
Chapter and Conference Paper
SSA Elimination after Register Allocation
Compilers such as gcc use static-single-assignment (SSA) form as an intermediate representation and usually perform SSA elimination before register allocation. But the order could as well be the opposite: the ...
-
Article
MEMOCODE 2006 guest editors’ introduction
-
Article
Improving the effectiveness of system verification
This special section presents three extended and revised papers which originally appeared in the proceedings of the 12th edition of the conference “Tools and Algorithms for the Construction and Analysis of Sys...
-
Chapter and Conference Paper
Verification of Register Allocators
A register allocator is difficult to write and debug. The task is to assign hardware registers to as many program variables as possible, assign memory locations to the rest, and avoid memory traffic to the ext...
-
Book and Conference Proceedings
Model Checking Software
15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008 Proceedings
-
Chapter
Efficient Type Matching
Palsberg and Zhao [25] presented an O(n 2) time algorithm for matching two recursive types; that is, deciding type isomorphism with associative-commutative product type constructors. In this paper, ...
-
Chapter and Conference Paper
Aliased Register Allocation for Straight-Line Programs Is NP-Complete
Register allocation is NP-complete in general but can be solved in linear time for straight-line programs where each variable has at most one definition point if the bank of registers is homogeneous. In this p...
-
Chapter and Conference Paper
A Framework for End-to-End Verification and Evaluation of Register Allocators
This paper presents a framework for designing, verifying, and evaluating register allocation algorithms. The proposed framework has three main components. The first component is MIRA, a language for describing...
-
Book and Conference Proceedings
Tools and Algorithms for the Construction and Analysis of Systems
12th International Conference, TACAS 2006, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2006, Vienna, Austria, March 25 - April 2, 2006. Proceedings
-
Chapter and Conference Paper
Event Driven Software Quality
Event-driven programming has found pervasive acceptance, from high-performance servers to embedded systems, as an efficient method for interacting with a complex world. The fastest research Web servers are eve...
