bluuebunny/crossref_metadata_2025 huggingface dataset:
Targeted coupon distribution using social networks
Authors: Shakkottai Srinivas , Ying Lei , Sah Sankalp
Published: January 2011

We propose to exploit online social networks in order to reveal user preferences such that goods and services might be targeted appropriately. We consider goods and services that are consumed periodically, and a user model where users could buy different numbers of goods at a marked ("high") price and at a discounted ("low") price. The problem is to identify users who are interested in the good, and to discount them sufficiently that the entire demand is realized, but not so much that revenue is compromised. Using techniques from "backpressure routing" used for control of multihop communication networks, we develop a multi-hop coupon forwarding scheme in which users are incentivized to forward the right number of coupons to appropriate neighbors such that the above target is achieved. We also develop a simple delay-based heuristic algorithm that also shows a near-optimal performance.
An architectural view of game theoretic control
Authors: Gopalakrishnan Ragavendran , Marden Jason R. , Wierman Adam
Published: January 2011

Game-theoretic control is a promising new approach for distributed resource allocation. In this paper, we describe how game-theoretic control can be viewed as having an intrinsic layered architecture, which provides a modularization that simplifies the control design. We illustrate this architectural view by presenting details about one particular instantiation using potential games as an interface. This example serves to highlight the strengths and limitations of the proposed architecture while also illustrating the relationship between game-theoretic control and other existing approaches to distributed resource allocation.
VM power metering
Authors: Krishnan Bhavani , Amur Hrishikesh , Gavrilovska Ada , Schwan Karsten
Published: January 2011

This paper explores the feasibility of and challenges in developing methods for black-box monitoring of the power usage of a virtual machine (VM) at run-time, on shared virtualized compute platforms, including those with complex memory hierarchies. We demonstrate that VM-level power utilization can be accurately estimated, or estimated with accuracy with bound error margins. The use of bounds permits more lightweight online monitoring of fewer events, while relaxing the fidelity of the estimates in a controlled manner. Our methodology is evaluated on the Intel Core i7 and Core2 x86-64 platforms, running synthetic and SPEC benchmarks.
Environmental impact of IEEE 802.11 access points
Authors: Sikdar Biplab
Published: January 2011

Wireless local area networks have become an ubiquitous means for network access in both residential and commercial locations over the recent past. Given their widespread deployment, it is of importance to understand their environmental impact and this paper presents a life cycle assessment of the energy intensity of IEEE 802.11 wireless access points. Following a cradle-to-grave approach, we evaluate the energy consumed in the manufacture of access points (including the extraction of raw materials, component manufacturing, assembly, and transportation) as well as during its actual usage. Our results show that the manufacturing stage is responsible for a significant fraction of the overall energy consumption. In light of our findings, increasing the overall lifetime is one of the recommended ways to reduce the environmental impact of access points.
A novel DTN based energy neutral transfer scheme for energy harvested WSN Gateways
Authors: Prabhakar T. V. , Nambi S.n Akshay Uttama , Jamadagni H. S. , Swaroop Krishna , Prasad R. Venkatesha , Niemegeers I. IG.M.M.
Published: January 2011

To overcome the problem of unavailability of grid power in rural India, we explore the possibility of powering WSN Gateways using a bicycle dynamo. The "data mule" bicycle generates its own power to ensure a self sustainable data transfer scheme to benefit small and marginal farmers. In our agricultural scenario, farmers have to generate electricity to get access to the technology. Our power measurements show that it is indeed possible to drive GPRS technologies with this power. We propose Transfer Energy Budget - a two way metric for gateway nodes to announce the available energy for relaying data. To achieve our goal, we exploit the DTN stack in the energy sense and introduce necessary modifications to its configuration. The results indicate that a 50 packet buffer has the least transfer energy budget with a data latency of about 31 seconds.
Teachers vs. Cell Phones
Authors: Klock Geoff
Published: January 2011

Four hundred years before Christ, Plato argued that technology, the written word itself, is distracting students from learning. Teachers today wish students would read a book sometime. The irony is stunning. As a professor, complaints that mobile phones distract from learning are ubiquitous. Text messaging, Facebook, and Twitter are the usual suspect applications.
Predictions for e-Learning in 2011
Authors: staff and contributors eLearn Magazine
Published: January 2011

At the start of each year, eLearn Magazine's editors, advisory board members, and other contributors predict what changes are afoot for the coming 12 months. Here are our predictions for 2011.
What Can You Gain by Teaching Online?
Authors: Everson Michelle
Published: January 2011

When I tell people I teach online discussion often turns, rather quickly, to all that a teacher will lose when teaching in the online environment. I will be the first to admit that there are certain things we often take for granted in a physical classroom that can be more of a challenge in the online environment. However it's time we focused more on what can be gained by teaching online rather than what could be lost.
Verified squared
Authors: Leroy Xavier
Published: January 2011

The formal verification of programs has progressed tremendously in the last decade. In this talk, I review some of the obstacles that [6, 8, 15, 18] remain to be lifted before source-level verification tools can be taken really seriously in the critical software industry. A direction I advocate is the systematic formal verification of the development tools that participate in the production and verification of critical software.
Points-to analysis with efficient strong updates
Authors: Lhoták Ondrej , Chung Kwok-Chiang Andrew
Published: January 2011

This paper explores a sweet spot between flow-insensitive and flow-sensitive subset-based points-to analysis. Flow-insensitive analysis is efficient: it has been applied to million-line programs and even its worst-case requirements are quadratic space and cubic time. Flow-sensitive analysis is precise because it allows strong updates, so that points-to relationships holding in one program location can be removed from the analysis when they no longer hold in other locations. We propose a "Strong Update" analysis combining both features: it is efficient like flow-insensitive analysis, with the same worst-case bounds, yet its precision benefits from strong updates like flow-sensitive analysis. The key enabling insight is that strong updates are applicable when the dereferenced points-to set is a singleton, and a singleton set is cheap to analyze. The analysis therefore focuses flow sensitivity on singleton sets. Larger sets, which will not lead to strong updates, are modelled flow insensitively to maintain efficiency. We have implemented and evaluated the analysis as an extension of the standard flow-insensitive points-to analysis in the LLVM compiler infrastructure.
Pick your contexts well
Authors: Smaragdakis Yannis , Bravenboer Martin , Lhoták Ondrej
Published: January 2011

Object-sensitivity has emerged as an excellent context abstraction for points-to analysis in object-oriented languages. Despite its practical success, however, object-sensitivity is poorly understood. For instance, for a context depth of 2 or higher, past scalable implementations deviate significantly from the original definition of an object-sensitive analysis. The reason is that the analysis has many degrees of freedom, relating to which context elements are picked at every method call and object creation. We offer a clean model for the analysis design space, and discuss a formal and informal understanding of object-sensitivity and of how to create good object-sensitive analyses. The results are surprising in their extent. We find that past implementations have made a sub-optimal choice of contexts, to the severe detriment of precision and performance. We define a "full-object-sensitive" analysis that results in significantly higher precision, and often performance, for the exact same context depth. We also introduce "type-sensitivity" as an explicit approximation of object-sensitivity that preserves high context quality at substantially reduced cost. A type-sensitive points-to analysis makes an unconventional use of types as context: the context types are not dynamic types of objects involved in the analysis, but instead upper bounds on the dynamic types of their allocator objects. Our results expose the influence of context choice on the quality of points-to analysis and demonstrate type-sensitivity to be an idea with major impact: It decisively advances the state-of-the-art with a spectrum of analyses that simultaneously enjoy speed (several times faster than an analogous object-sensitive analysis), scalability (comparable to analyses with much less context-sensitivity), and precision (comparable to the best object-sensitive analysis with the same context depth).
Relaxed-memory concurrency and verified compilation
Authors: Ŝevčik Jaroslav , Vafeiadis Viktor , Zappa Nardelli Francesco , Jagannathan Suresh , Sewell Peter
Published: January 2011

In this paper, we consider the semantic design and verified compilation of a C-like programming language for concurrent shared-memory computation above x86 multiprocessors. The design of such a language is made surprisingly subtle by several factors: the relaxed-memory behaviour of the hardware, the effects of compiler optimisation on concurrent code, the need to support high-performance concurrent algorithms, and the desire for a reasonably simple programming model. In turn, this complexity makes verified (or verifying) compilation both essential and challenging.

We define a concurrent relaxed-memory semantics for
ClightTSO
, an extension of CompCert's Clight in which the processor's memory model is exposed for high-performance code. We discuss a strategy for verifying compilation from ClightTSO to x86, which we validate with correctness proofs (building on CompCert) for the most interesting compiler phases.
Formal verification of object layout for c++ multiple inheritance
Authors: Ramananandro Tahina , Dos Reis Gabriel , Leroy Xavier
Published: January 2011

Object layout - the concrete in-memory representation of objects - raises many delicate issues in the case of the C++ language, owing in particular to multiple inheritance, C compatibility and separate compilation. This paper formalizes a family of C++ object layout schemes and mechanically proves their correctness against the operational semantics for multiple inheritance of Wasserrab et al. This formalization is flexible enough to account for space-saving techniques such as empty base class optimization and tail-padding optimization. As an application, we obtain the first formal correctness proofs for realistic, optimized object layout algorithms, including one based on the popular "common vendor" Itanium C++ application binary interface. This work provides semantic foundations to discover and justify new layout optimizations; it is also a first step towards the verification of a C++ compiler front-end.
Step-indexed kripke models over recursive worlds
Authors: Birkedal Lars , Reus Bernhard , Schwinghammer Jan , Støvring Kristian , Thamsborg Jacob , Yang Hongseok
Published: January 2011

Over the last decade, there has been extensive research on modelling challenging features in programming languages and program logics, such as higher-order store and storable resource invariants. A recent line of work has identified a common solution to some of these challenges: Kripke models over worlds that are recursively defined in a category of metric spaces. In this paper, we broaden the scope of this technique from the original domain-theoretic setting to an elementary, operational one based on step indexing. The resulting method is widely applicable and leads to simple, succinct models of complicated language features, as we demonstrate in our semantics of Charguéraud and Pottier's type-and-capability system for an ML-like higher-order language. Moreover, the method provides a high-level understanding of the essence of recent approaches based on step indexing.
Calling context abstraction with shapes
Authors: Rival Xavier , Chang Bor-Yuh Evan
Published: January 2011

Interprocedural program analysis is often performed by computing procedure summaries. While possible, computing adequate summaries is difficult, particularly in the presence of recursive procedures. In this paper, we propose a complementary framework for interprocedural analysis based on a direct abstraction of the calling context. Specifically, our approach exploits the inductive structure of a calling context by treating it directly as a stack of activation records. We then build an abstraction based on separation logic with inductive definitions. A key element of this abstract domain is the use of parameters to refine the meaning of such call stack summaries and thus express relations across activation records and with the heap. In essence, we define an abstract interpretation-based analysis framework for recursive programs that permits a fluid per call site abstraction of the call stack--much like how shape analyzers enable a fluid per program point abstraction of the heap.
Precise reasoning for programs using containers
Authors: Dillig Isil , Dillig Thomas , Aiken Alex
Published: January 2011

Containers are general-purpose data structures that provide functionality for inserting, reading, removing, and iterating over elements. Since many applications written in modern programming languages, such as C++ and Java, use containers as standard building blocks, precise analysis of many programs requires a fairly sophisticated understanding of container contents. In this paper, we present a sound, precise, and fully automatic technique for static reasoning about contents of containers. We show that the proposed technique adds useful precision for verifying real C++ applications and that it scales to applications with over 100,000 lines of code.
Modular reasoning for deterministic parallelism
Authors: Dodds Mike , Jagannathan Suresh , Parkinson Matthew J.
Published: January 2011

Weaving a concurrency control protocol into a program is difficult and error-prone. One way to alleviate this burden is
deterministic parallelism
. In this well-studied approach to parallelisation, a sequential program is annotated with sections that can execute concurrently, with automatically injected control constructs used to ensure observable behaviour consistent with the original program.

This paper examines the formal specification and verification of these constructs. Our high-level specification defines the conditions necessary for correct execution; these conditions reflect program dependencies necessary to ensure deterministic behaviour. We connect the high-level specification used by clients of the library with the low-level library implementation, to prove that a client's requirements for determinism are enforced. Significantly, we can reason about program and library correctness without breaking abstraction boundaries.

To achieve this, we use
concurrent abstract predicates
, based on separation logic, to encapsulate racy behaviour in the library's implementation. To allow generic specifications of libraries that can be instantiated by client programs, we extend the logic with higher-order parameters and quantification. We show that our high-level specification abstracts the details of deterministic parallelism by verifying two different low-level implementations of the library.
Fresh-register automata
Authors: Tzevelekos Nikos
Published: January 2011

What is a basic automata-theoretic model of computation with names and fresh-name generation?
We introduce Fresh-Register Automata (FRA), a new class of automata which operate on an infinite alphabet of names and use a finite number of registers to store fresh names, and to compare incoming names with previously stored ones. These finite machines extend Kaminski and Francez's Finite-Memory Automata by being able to recognise globally fresh inputs, that is, names fresh in the whole current run. We examine the expressivity of FRA's both from the aspect of accepted languages and of bisimulation equivalence. We establish primary properties and connections between automata of this kind, and answer key decidability questions. As a demonstrating example, we express the theory of the pi-calculus in FRA's and characterise bisimulation equivalence by an appropriate, and decidable in the finitary case, notion in these automata.
Vector addition system reachability problem
Authors: Leroux Jérôme
Published: January 2011

The reachability problem for Vector Addition Systems (VASs) is a central problem of net theory. The general problem is known decidable by algorithms exclusively based on the classical Kosaraju-Lambert-Mayr-Sacerdote-Tenney decomposition (KLMTS decomposition). Recently from this decomposition, we deduced that a final configuration is not reachable from an initial one if and only if there exists a Presburger inductive invariant that contains the initial configuration but not the final one. Since we can decide if a Preburger formula denotes an inductive invariant, we deduce from this result that there exist checkable certificates of non-reachability in the Presburger arithmetic. In particular, there exists a simple algorithm for deciding the general VAS reachability problem based on two semi-algorithms. A first one that tries to prove the reachability by enumerating finite sequences of actions and a second one that tries to prove the non-reachability by enumerating Presburger formulas. In this paper we provide the first proof of the VAS reachability problem that is not based on the KLMST decomposition. The proof is based on the notion of production relations inspired from Hauschildt that directly provides the existence of Presburger inductive invariants.
Symmetric lenses
Authors: Hofmann Martin , Pierce Benjamin , Wagner Daniel
Published: January 2011

Lenses
--bidirectional transformations between pairs of connected structures--have been extensively studied and are beginning to find their way into industrial practice. However, some aspects of their foundations remain poorly understood. In particular, most previous work has focused on the special case of
asymmetric lenses
, where one of the structures is taken as primary and the other is thought of as a projection, or view. A few studies have considered symmetric variants, where each structure contains information not present in the other, but these all lack the basic operation of
composition
. Moreover, while many domain-specific languages based on lenses have been designed, lenses have not been thoroughly explored from an algebraic perspective.

We offer two contributions to the theory of lenses. First, we present a new symmetric formulation, based on
complements
, an old idea from the database literature. This formulation generalizes the familiar structure of asymmetric lenses, and it admits a good notion of composition. Second, we explore the algebraic structure of the space of symmetric lenses. We present generalizations of a number of known constructions on asymmetric lenses and settle some longstanding questions about their properties---in particular, we prove the existence of (symmetric monoidal) tensor products and sums and the
non
-existence of full categorical products or sums in the category of symmetric lenses. We then show how the methods of universal algebra can be applied to build
iterator lenses
for structured data such as lists and trees, yielding lenses for operations like mapping, filtering, and concatenation from first principles. Finally, we investigate an even more general technique for constructing mapping combinators, based on the theory of
containers
.
Regular expression containment
Authors: Henglein Fritz , Nielsen Lasse
Published: January 2011

We present a new sound and complete axiomatization of regular expression containment. It consists of the conventional axiomatization of concatenation, alternation, empty set and (the singleton set containing) the empty string as an idempotent semiring, the fixed- point rule
E
* = 1 +
E
×
E
* for Kleene-star, and a general coinduction rule as the only additional rule.

Our axiomatization gives rise to a natural computational interpretation of regular expressions as simple types that represent parse trees, and of containment proofs as
coercions
. This gives the axiom- atization a Curry-Howard-style constructive interpretation: Containment proofs do not only certify a language-theoretic contain- ment, but, under our computational interpretation, constructively transform a membership proof of a string in one regular expression into a membership proof of the same string in another regular expression.

We show how to encode regular expression equivalence proofs in Salomaa's, Kozen's and Grabmayer's axiomatizations into our containment system, which equips their axiomatizations with a computational interpretation and implies completeness of our axiomatization. To ensure its soundness, we require that the computational interpretation of the coinduction rule be a hereditarily total function. Hereditary totality can be considered the mother of syn- tactic side conditions: it "explains" their soundness, yet cannot be used as a conventional side condition in its own right since it turns out to be undecidable.

We discuss application of
regular expressions as types
to bit coding of strings and hint at other applications to the wide-spread use of regular expressions for substring matching, where classical automata-theoretic techniques are
a priori
inapplicable.

Neither regular expressions as types nor subtyping interpreted coercively are novel
per se
. Somewhat surprisingly, this seems to be the first investigation of a general proof-theoretic framework for the latter in the context of the former, however.
Making prophecies with decision predicates
Authors: Cook Byron , Koskinen Eric
Published: January 2011

We describe a new algorithm for proving temporal properties expressed in LTL of infinite-state programs. Our approach takes advantage of the fact that LTL properties can often be proved more efficiently using techniques usually associated with the branching-time logic CTL than they can with native LTL algorithms. The caveat is that, in certain instances, nondeterminism in the system's transition relation can cause CTL methods to report counter examples that are spurious with respect to the original LTL formula. To address this problem we describe an algorithm that, as it attempts to apply CTL proof methods, finds and then removes problematic nondeterminism via an analysis on the potentially spurious counterexamples. Problematic nondeterminism is characterized using
decision predicates
, and removed using a partial, symbolic determinization procedure which introduces new prophecy variables to predict the future outcome of these choices. We demonstrate---using examples taken from the PostgreSQL database server, Apache web server, and Windows OS kernel---that our method can yield enormous performance improvements in comparison to known tools, allowing us to automatically prove properties of programs where we could not prove them before.
On interference abstractions
Authors: Sinha Nishant , Wang Chao
Published: January 2011

Interference is the bane of both concurrent programming and analysis. To avoid considering all possible interferences between concurrent threads, most automated static analysis employ techniques to approximate interference, e.g., by restricting the thread scheduler choices or by approximating the transition relations or reachable states of the program. However, none of these methods are able to reason about interference directly. In this paper, we introduce the notion of
interference abstractions
(IAs), based on the models of shared memory consistency, to reason about interference efficiently. IAs differ from the known abstractions for concurrent programs and cannot be directly modeled by these abstractions. Concurrency bugs typically involve a small number of unexpected interferences and therefore can be captured by small IAs. We show how IAs, in the form of both over- and under-approximations of interference, can be obtained syntactically from the axioms of sequential consistency. Further, we present an automatic method to synthesize IAs suitable for checking safety properties. Our experimental results show that small IAs are often sufficient to check properties in realistic applications, and drastically improve the scalability of concurrent program analysis in these applications.
Practical affine types
Authors: Tov Jesse A. , Pucella Riccardo
Published: January 2011

Alms is a general-purpose programming language that supports practical affine types. To offer the expressiveness of Girard's linear logic while keeping the type system light and convenient, Alms uses expressive kinds that minimize notation while maximizing polymorphism between affine and unlimited types.

A key feature of Alms is the ability to introduce abstract affine types via ML-style signature ascription. In Alms, an interface can impose stiffer resource usage restrictions than the principal usage restrictions of its implementation. This form of sealing allows the type system to naturally and directly express a variety of resource management protocols from special-purpose type systems.

We present two pieces of evidence to demonstrate the validity of our design goals. First, we introduce a prototype implementation of Alms and discuss our experience programming in the language. Second, we establish the soundness of the core language. We also use the core model to prove a principal kinding theorem.
Space overhead bounds for dynamic memory management with partial compaction
Authors: Bendersky Anna , Petrank Erez
Published: January 2011

Dynamic memory allocation is ubiquitous in today's runtime environments. Allocation and de-allocation of objects during program execution may cause fragmentation and foil the program's ability to allocate objects. Robson has shown that a worst case scenario can create a space overhead within a factor of log(n) of the space that is actually required by the program, where n is the size of the largest possible object. Compaction can eliminate fragmentation, but is too costly to be run frequently. Many runtime systems employ partial compaction, in which only a small fraction of the allocated objects are moved. Partial compaction reduces some of the existing fragmentation at an acceptable cost. In this paper we study the effectiveness of partial compaction and provide the first rigorous lower and upper bounds on its effectiveness in reducing fragmentation at a low cost.
Laws of order
Authors: Attiya Hagit , Guerraoui Rachid , Hendler Danny , Kuznetsov Petr , Michael Maged M. , Vechev Martin
Published: January 2011

Building correct and efficient concurrent algorithms is known to be a difficult problem of fundamental importance. To achieve efficiency, designers try to remove unnecessary and costly synchronization. However, not only is this manual trial-and-error process ad-hoc, time consuming and error-prone, but it often leaves designers pondering the question of: is it inherently impossible to eliminate certain synchronization, or is it that I was unable to eliminate it on this attempt and I should keep trying?

In this paper we respond to this question. We prove that it is impossible to build concurrent implementations of classic and ubiquitous specifications such as sets, queues, stacks, mutual exclusion and read-modify-write operations, that completely eliminate the use of expensive synchronization.

We prove that one cannot avoid the use of either: i) read-after-write (RAW), where a write to shared variable A is followed by a read to a different shared variable B without a write to B in between, or ii) atomic write-after-read (AWAR), where an atomic operation reads and then writes to shared locations. Unfortunately, enforcing RAW or AWAR is expensive on all current mainstream processors. To enforce RAW, memory ordering--also called fence or barrier--instructions must be used. To enforce AWAR, atomic instructions such as compare-and-swap are required. However, these instructions are typically substantially slower than regular instructions.

Although algorithm designers frequently struggle to avoid RAW and AWAR, their attempts are often futile. Our result characterizes the cases where avoiding RAW and AWAR is impossible. On the flip side, our result can be used to guide designers towards new algorithms where RAW and AWAR can be eliminated.
Complexity of pattern-based verification for multithreaded programs
Authors: Esparza Javier , Ganty Pierre
Published: January 2011

Pattern-based verification checks the correctness of the program executions that follow a given
pattern
, a regular expression over the alphabet of program transitions of the form
w
1
* ...
w
n
*. For multithreaded programs, the alphabet of the pattern is given by the synchronization operations between threads. We study the complexity of pattern-based verification for
abstracted
multithreaded programs in which, as usual in program analysis, conditions have been replaced by nondeterminism (the technique works also for boolean programs). While unrestricted verification is undecidable for abstracted multithreaded programs with recursive procedures and PSPACE-complete for abstracted multithreaded while-programs, we show that pattern-based verification is NP-complete for both classes. We then conduct a multiparameter analysis in which we study the complexity in the number of threads, the number of procedures per thread, the size of the procedures, and the size of the pattern. We first show that no algorithm for pattern-based verification can be polynomial in the number of threads, procedures per thread, or the size of the pattern (unless P=NP). Then, using recent results about Parikh images of regular languages and semilinear sets, we present an algorithm exponential in the number of threads, procedures per thread, and size of the pattern, but polynomial in the size of the procedures.
EigenCFA
Authors: Prabhu Tarun , Ramalingam Shreyas , Might Matthew , Hall Mary
Published: January 2011

We describe, implement and benchmark EigenCFA, an algorithm for accelerating higher-order control-flow analysis (specifically, 0CFA) with a GPU. Ultimately, our program transformations, reductions and optimizations achieve a factor of 72 speedup over an optimized CPU implementation.

We began our investigation with the view that GPUs accelerate high-arithmetic, data-parallel computations with a poor tolerance for branching. Taking that perspective to its limit, we reduced Shivers's abstract-interpretive 0CFA to an algorithm synthesized from linear-algebra operations. Central to this reduction were "abstract" Church encodings, and encodings of the syntax tree and abstract domains as vectors and matrices.

A straightforward (dense-matrix) implementation of EigenCFA performed slower than a fast CPU implementation. Ultimately, sparse-matrix data structures and operations turned out to be the critical accelerants. Because control-flow graphs are sparse in practice (up to 96% empty), our control-flow matrices are also sparse, giving the sparse matrix operations an overwhelming space and speed advantage.

We also achieved speedups by carefully permitting data races. The monotonicity of 0CFA makes it sound to perform analysis operations in parallel, possibly using stale or even partially-updated data.
Safe nondeterminism in a deterministic-by-default parallel language
Authors: Bocchino Robert L. , Heumann Stephen , Honarmand Nima , Adve Sarita V. , Adve Vikram S. , Welc Adam , Shpeisman Tatiana
Published: January 2011

A number of deterministic parallel programming models with strong safety guarantees are emerging, but similar support for nondeterministic algorithms, such as branch and bound search, remains an open question. We present a language together with a type and effect system that supports nondeterministic computations with a deterministic-by-default guarantee: nondeterminism must be explicitly requested via special parallel constructs (marked nd), and any deterministic construct that does not execute any nd construct has deterministic input-output behavior. Moreover, deterministic parallel constructs are always equivalent to a sequential composition of their constituent tasks, even if they enclose, or are enclosed by, nd constructs. Finally, in the execution of nd constructs, interference may occur only between pairs of accesses guarded by atomic statements, so there are no data races, either between atomic statements and unguarded accesses (strong isolation) or between pairs of unguarded accesses (stronger than strong isolation alone). We enforce the guarantees at compile time with modular checking using novel extensions to a previously described effect system. Our effect system extensions also enable the compiler to remove unnecessary transactional synchronization. We provide a static semantics, dynamic semantics, and a complete proof of soundness for the language, both with and without the barrier removal feature. An experimental evaluation shows that our language can achieve good scalability for realistic parallel algorithms, and that the barrier removal techniques provide significant performance gains.
The essence of compiling with traces
Authors: Guo Shu-yu , Palsberg Jens
Published: January 2011

The technique of trace-based just-in-time compilation was introduced by Bala et al. and was further developed by Gal et al. It currently enjoys success in Mozilla Firefox's JavaScript engine. A trace-based JIT compiler leverages run-time profiling to optimize frequently-executed paths while enabling the optimized code to ``bail out'' to the original code when the path has been invalidated. This optimization strategy differs from those of other JIT compilers and opens the question of
which trace optimizations are sound
. In this paper we present a framework for reasoning about the soundness of trace optimizations, and we show that some traditional optimization techniques are sound when used in a trace compiler while others are unsound. The converse is also true: some trace optimizations are sound when used in a traditional compiler while others are unsound. So, traditional and trace optimizations form incomparable sets. Our setting is an imperative calculus for which tracing is explicitly spelled out in the semantics. We define optimization soundness via a notion of bisimulation, and we show that sound optimizations lead to confluence and determinacy of stores.
Streaming transducers for algorithmic verification of single-pass list-processing programs
Authors: Alur Rajeev , Černý Pavol
Published: January 2011

We introduce
streaming data string transducers
that map input data strings to output data strings in a single left-to-right pass in linear time. Data strings are (unbounded) sequences of data values, tagged with symbols from a finite set, over a potentially infinite data domain that supports only the operations of equality and ordering. The transducer uses a finite set of states, a finite set of variables ranging over the data domain, and a finite set of variables ranging over data strings. At every step, it can make decisions based on the next input symbol, updating its state, remembering the input data value in its data variables, and updating data-string variables by concatenating data-string variables and new symbols formed from data variables, while avoiding duplication. We establish PSPACE bounds for the problems of checking functional equivalence of two streaming transducers, and of checking whether a streaming transducer satisfies pre/post verification conditions specified by streaming acceptors over input/output data-strings.

We identify a class of imperative and a class of functional programs, manipulating lists of data items, which can be effectively translated to streaming data-string transducers. The imperative programs dynamically modify a singly-linked heap by changing next-pointers of heap-nodes and by adding new nodes. The main restriction specifies how the next-pointers can be used for traversal. We also identify an expressively equivalent fragment of functional programs that traverse a list using syntactically restricted recursive calls. Our results lead to algorithms for assertion checking and for checking functional equivalence of two programs, written possibly in different programming styles, for commonly used routines such as insert, delete, and reverse.
Decidable logics combining heap structures and data
Authors: Madhusudan P. , Parlato Gennaro , Qiu Xiaokang
Published: January 2011

We define a new logic, STRAND, that allows reasoning with heap-manipulating programs using deductive verification and SMT solvers. STRAND logic ("STRucture ANd Data" logic) formulas express constraints involving heap structures and the data they contain; they are defined over a class of pointer-structures
R
defined using MSO-defined relations over trees, and are of the form ∃→
x
∀→
y
(→
x
,→)
x
" , where "φ" is a monadic second-order logic (MSO) formulawith additional quantification that combines structural constraints as well as data-constraints, but where the data-constraints are only allowed to refer to "→
x
" and "→
y
"

The salient aspects of the logic are: (a) the logic is powerful, allowing existential and universal quantification over the nodes, and complex combinations of data and structural constraints; (b) checking Hoare-triples for linear blocks of statements with pre-conditions and post-conditions expressed as Boolean combinations of existential and universal STRAND formulas reduces to satisfiability of a STRAND formula; (c) there are powerful decidable fragments of STRAND, one semantically defined and one syntactically defined, where the decision procedure works by combining the theory of MSO over trees and the quantifier-free theory of the underlying data-logic. We demonstrate the effectiveness and practicality of the logic by checking verification conditions generated in proving properties of several heap-manipulating programs, using a tool that combines an MSO decision procedure over trees (MONA) with an SMT solver for integer constraints (Z3).
A technique for the effective and automatic reuse of classical compiler optimizations on multithreaded code
Authors: Joisha Pramod G. , Schreiber Robert S. , Banerjee Prithviraj , Boehm Hans J. , Chakrabarti Dhruva R.
Published: January 2011

A large body of data-flow analyses exists for analyzing and optimizing sequential code. Unfortunately, much of it cannot be directly applied on parallel code, for reasons of correctness. This paper presents a technique to automatically, aggressively, yet safely apply sequentially-sound data-flow transformations,
without change
, on shared-memory programs. The technique is founded on the notion of program references being "siloed" on certain control-flow paths. Intuitively, siloed references are free of interference from other threads within the confines of such paths. Data-flow transformations can, in general, be unblocked on siloed references.

The solution has been implemented in a widely used compiler. Results on benchmarks from SPLASH-2 show that performance improvements of up to 41% are possible, with an average improvement of 6% across all the tested programs over all thread counts.
Measured impact of crooked traceroute
Authors: Luckie Matthew , Dhamdhere Amogh , claffy kc , Murrell David
Published: January 2011

Data collected using traceroute-based algorithms underpins research into the Internet's router-level topology, though it is possible to infer false links from this data. One source of false inference is the combination of per-flow load-balancing, in which more than one path is active from a given source to destination, and classic traceroute, which varies the UDP destination port number or ICMP checksum of successive probe packets, which can cause per-flow load-balancers to treat successive packets as distinct flows and forward them along different paths. Consequently, successive probe packets can solicit responses from unconnected routers, leading to the inference of false links. This paper examines the inaccuracies induced from such false inferences, both on macroscopic and ISP topology mapping. We collected macroscopic topology data to 365k destinations, with techniques that both do and do not try to capture load balancing phenomena. We then use alias resolution techniques to infer if a measurement artifact of classic traceroute induces a false router-level link. This technique detected that 2.71% and 0.76% of the links in our UDP and ICMP graphs were falsely inferred due to the presence of load-balancing. We conclude that most per-flow load-balancing does not induce false links when macroscopic topology is inferred using classic traceroute. The effect of false links on ISP topology mapping is possibly much worse, because the degrees of a tier-1 ISP's routers derived from classic traceroute were inflated by a median factor of 2.9 as compared to those inferred with Paris traceroute.
Papyrus
Authors: Yang Lei , Zhang Zengbin , Hou Wei , Zhao Ben Y. , Zheng Haitao
Published: January 2011

Proliferation and innovation of wireless technologies require significant amounts of radio spectrum. Recent policy reforms by the FCC are paving the way by freeing up spectrum for a new generation of frequency-agile wireless devices based on software defined radios (SDRs). But despite recent advances in SDR hardware, research on SDR MAC protocols or applications requires an experimental platform for managing physical access. We introduce Papyrus, a software platform for wireless researchers to develop and experiment dynamic spectrum systems using currently available SDR hardware. Papyrus provides two fundamental building blocks at the physical layer: flexible non-contiguous frequency access and simple and robust frequency detection. Papyrus allows researchers to deploy and experiment new MAC protocols and applications on USRP GNU Radio, and can also be ported to other SDR platforms. We demonstrate the use of Papyrus using Jello, a distributed MAC overlay for high-bandwidth media streaming applications and Ganache, a SDR layer for adaptable guardband configuration. Full implementations of Papyrus and Jello are publicly available.
Tool release
Authors: Halperin Daniel , Hu Wenjun , Sheth Anmol , Wetherall David
Published: January 2011

We are pleased to announce the release of a tool that records detailed measurements of the wireless channel along with received 802.11 packet traces. It runs on a commodity 802.11n NIC, and records Channel State Information (CSI) based on the 802.11 standard. Unlike Receive Signal Strength Indicator (RSSI) values, which merely capture the total power received at the listener, the CSI contains information about the channel between sender and receiver at the level of individual data subcarriers, for each pair of transmit and receive antennas.

Our toolkit uses the Intel WiFi Link 5300 wireless NIC with 3 antennas. It works on up-to-date Linux operating systems: in our testbed we use Ubuntu 10.04 LTS with the 2.6.36 kernel. The measurement setup comprises our customized versions of Intel's close-source firmware and open-source iwlwifi wireless driver, userspace tools to enable these measurements, access point functionality for controlling both ends of the link, and Matlab (or Octave) scripts for data analysis. We are releasing the binary of the modified firmware, and the source code to all the other components.
AirLab
Authors: Kone Vinod , Zheleva Mariya , Wittie Mile , Zhao Ben Y. , Belding Elizabeth M. , Zheng Haitao , Almeroth Kevin
Published: January 2011

Accurate measurements of deployed wireless networks are vital for researchers to perform realistic evaluation of proposed systems. Unfortunately, the difficulty of performing detailed measurements limits the consistency in parameters and methodology of current datasets. Using different datasets, multiple research studies can arrive at conflicting conclusions about the performance of wireless systems. Correcting this situation requires consistent and comparable wireless traces collected from a variety of deployment environments. In this paper, we describe AirLab, a distributed wireless data collection infrastructure that uses uniformly instrumented measurement nodes at heterogeneous locations to collect consistent traces of both standardized and user-defined experiments. We identify four challenges in the AirLab platform, consistency, fidelity, privacy, security, and describe our approaches to address them.
Session reports for SIGCOMM 2010
Authors: Agrawal Shailesh , Athota Kavitha , Bhatotia Pramod , Goyal Piyush , Krisha Phani , Ruchandan Kirtika , Sastry Nishanth , Singh Gurmeet , Sudevalayam Sujesha , Thomas Immanuel Ilavarasan , Vishwanath Arun , Xu Tianyin , Yu Fang
Published: January 2011

This document collects together reports of the sessions from the 2010 ACM SIGCOMM Conference, the annual conference of the ACM Special Interest Group on Data Communication (SIGCOMM) on the applications, technologies, architectures, and protocols for computer communication.
Architecture optimisation with currawong
Authors: FitzRoy-Dale Nicholas , Kuz Ihor , Heiser Gernot
Published: January 2011

We describe Currawong, a tool to perform
system software architecture optimisation
. Currawong is an extensible tool which applies optimisations at the point where an application invokes framework or library code. Currawong does not require source code to perform optimisations, effectively decoupling the relationship between compilation and optimisation. We show, through examples written for the popular Android smartphone platform, that Currawong is capable of significant performance improvement to existing applications.
Topology-aware resource allocation for data-intensive workloads
Authors: Lee Gunho , Tolia Niraj , Ranganathan Parthasarathy , Katz Randy H.
Published: January 2011

This paper proposes an architecture for optimized resource allocation in Infrastructure-as-a-Service (IaaS)-based cloud systems. Current IaaS systems are usually unaware of the hosted application's requirements and therefore allocate resources independently of its needs, which can significantly impact performance for distributed data-intensive applications.

To address this resource allocation problem, we propose an architecture that adopts a what if methodology to guide allocation decisions taken by the IaaS. The architecture uses a prediction engine with a lightweight simulator to estimate the performance of a given resource allocation and a genetic algorithm to find an optimized solution in the large search space. We have built a prototype for Topology-Aware Resource Allocation (TARA) and evaluated it on a 80 server cluster with two representative MapReduce-based benchmarks. Our results show that TARA reduces the job completion time of these applications by up to 59% when compared to application-independent allocation policies.