bluuebunny/crossref_metadata_2025 huggingface dataset:
Electromagnetic Casimir densities for a cylindrical shell on de Sitter space
Authors: Saharian A. A. , Manukyan V. F. , Saharyan N. A.
Published: December 2016

Complete set of cylindrical modes is constructed for the electromagnetic field inside and outside a cylindrical shell in the background of [Formula: see text]-dimensional dS space–time. On the shell, the field obeys the generalized perfect conductor boundary condition. For the Bunch–Davies vacuum state, we evaluate the vacuum expectation values (VEVs) of the electric field squared and of the energy–momentum tensor. The shell-induced contributions are explicitly extracted. In this way, for points away from the shell, the renormalization is reduced to the one for the VEVs in the boundary-free dS bulk. As a special case, the VEVs are obtained for a cylindrical shell in the [Formula: see text]-dimensional Minkowski bulk. We show that the shell-induced contribution in the electric field squared is positive for both the interior and exterior regions. The corresponding Casimir–Polder forces are directed toward the shell. The vacuum energy–momentum tensor, in addition to the diagonal components, has a nonzero off-diagonal component corresponding to the energy flux along the direction normal to the shell. This flux is directed from the shell in both the exterior and interior regions. For points near the shell, the leading terms in the asymptotic expansions for the electric field squared and diagonal components of the energy–momentum tensor are obtained from the corresponding expressions in the Minkowski bulk replacing the distance from the shell by the proper distance in the dS bulk. The influence of the gravitational field on the local characteristics of the vacuum is essential at distances from the shell larger than the dS curvature radius. The results are extended for confining boundary conditions of flux tube models in QCD.
The effects of Rashba spin–orbit coupling and Holstein phonons on thermodynamic properties of BN-doped graphene
Authors: Yarmohammadi Mohsen , Mirabbaszadeh Kavoos , Shirzadi Bahram
Published: December 2016

Starting from the Holstein model, we have investigated the effects of Rashba spin–orbit coupling (RSOC) on density of states (DOS), electronic heat capacity (EHC) and magnetic susceptibility (MS) of boron nitride-doped (BN-doped) graphene beyond the Dirac cone approximation within the Green’s function approach. By using the self-consistent perturbation theory, retarded self-energy can be calculated. We have found that the band gap (the peak of EHC and MS) of the system increases (decreases) with RSOC and electron–phonon (e–ph) interaction. Also, the Schottky anomaly moves only to the higher temperatures for strong RSOCs and e–ph interactions. Also, our results show that the response of the system to an external magnetic field is scaled down in the presence of RSOC and e–ph interaction.
IEEE754 Precision-
k
base-β Arithmetic Inherited by Precision-
m
Base-β Arithmetic for
k
<
m
Authors: Rump Siegfried M.
Published: December 2016

Suppose an
m
-digit floating-point arithmetic in base β ≥ 2 following the IEEE754 arithmetic standard is available. We show how a
k
-digit arithmetic with
k
<
m
can be inherited solely using
m
-digit operations. This includes the rounding into
k
digits, the four basic operations and the square root, all for even or odd base β. In particular, we characterize the relation between
k
and
m
so that no double rounding occurs when computing in
m
digits and rounding the result into
k
digits. We discuss rounding to nearest as well as directed rounding, and our approach covers exceptional values including signed zero. For binary arithmetic, a Matlab toolbox based on binary64 including
k
-bit scalar, vector and matrix operations as well as
k
-bit interval arithmetic is part of Version 8 of INTLAB, the Matlab toolbox for reliable computing.
Algorithm 968
Authors: Calvo Manuel , Montijano Juan I. , Rández Luis
Published: December 2016

In this article, an adaptive Runge-Kutta code, based on the DOPRI5(4) pair for solving initial value problems (IVPs) for differential systems with piecewise smooth solutions (PWS) is presented and the algorithms used in the code are described. The code automatically detects and locates accurately the switching points of the PWS, restarting the integration after each discontinuity. Further, in the case of Filippov systems, algorithms to handle properly sliding mode regimes in an automatic way are included. The code requires the user to provide a description of the IVP and the functions defining the hypersurfaces where the switching points are located, and it returns the discrete approximated solution together with the switching points. Several numerical experiments are presented to illustrate the reliability and efficiency of the code.
Ghostbuster: a tool for simplifying and converting GADTs
Authors: McDonell Trevor L. , Zakian Timothy A. K. , Cimini Matteo , Newton Ryan R.
Published: December 2016

Generalized Algebraic Dataypes, or simply GADTs, can encode non-trivial properties in the types of the constructors. Once such properties are encoded in a datatype, however, all code manipulating that datatype must provide proof that it maintains these properties in order to typecheck. In this paper, we take a step towards gradualizing these obligations. We introduce a tool, Ghostbuster, that produces simplified versions of GADTs which elide selected type parameters, thereby weakening the guarantees of the simplified datatype in exchange for reducing the obligations necessary to manipulate it. Like ornaments, these simplified datatypes preserve the recursive structure of the original, but unlike ornaments we focus on information-preserving bidirectional transformations. Ghostbuster generates type-safe conversion functions between the original and simplified datatypes, which we prove are the identity function when composed. We evaluate a prototype tool for Haskell against thousands of GADTs found on the Hackage package database, generating simpler Haskell'98 datatypes and round-trip conversion functions between the two.
Unifiers as equivalences: proof-relevant unification of dependently typed data
Authors: Cockx Jesper , Devriese Dominique , Piessens Frank
Published: December 2016

Dependently typed languages such as Agda, Coq and Idris use a syntactic first-order unification algorithm to check definitions by dependent pattern matching. However, these algorithms don’t adequately consider the types of the terms being unified, leading to various unintended results. As a consequence, they require ad hoc restrictions to preserve soundness, but this makes them very hard to prove correct, modify, or extend.

This paper proposes a framework for reasoning formally about unification in a dependently typed setting. In this framework, unification rules compute not just a unifier but also a corresponding correctness proof in the form of an equivalence between two sets of equations. By rephrasing the standard unification rules in a proof-relevant manner, they are guaranteed to preserve soundness of the theory. In addition, it enables us to safely add new rules that can exploit the dependencies between the types of equations.

Using our framework, we reimplemented the unification algorithm used by Agda. As a result, we were able to replace previous ad hoc restrictions with formally verified unification rules, fixing a number of bugs in the process. We are convinced this will also enable the addition of new and interesting unification rules in the future, without compromising soundness along the way.
Compact bit encoding schemes for simply-typed lambda-terms
Authors: Takeda Kotaro , Kobayashi Naoki , Yaguchi Kazuya , Shinohara Ayumi
Published: December 2016

We consider the problem of how to compactly encode simply-typed λ-terms into bit strings. The work has been motivated by Kobayashi et al.’s recent work on higher-order data compression, where data are encoded as functional programs (or, λ-terms) that generate them. To exploit its good compression power, the compression scheme has to come with a method for compactly encoding the λ-terms into bit strings. To this end, we propose two type-based bit-encoding schemes; the first one encodes a λ-term into a sequence of symbols by using type information, and then applies arithmetic coding to convert the sequence to a bit string. The second one is more sophisticated; we prepare a context-free grammar (CFG) that describes only well-typed terms, and then use a variation of arithmetic coding specialized for the CFG. We have implemented both schemes and confirmed that they often output more compact codes than previous bit encoding schemes for λ-terms.
Deriving a probability density calculator (functional pearl)
Authors: Mohammed Ismail Wazim , Shan Chung-chieh
Published: December 2016

Given an expression that denotes a probability distribution, often we want a corresponding
density
function, to use in probabilistic inference. Fortunately, the task of finding a density has been automated. It turns out that we can
derive
a compositional procedure for finding a density, by equational reasoning about integrals, starting with the mathematical specification of what a density is. Moreover, the density found can be run as an estimation algorithm, as well as simplified as an exact formula to improve the estimate.
Context-free session types
Authors: Thiemann Peter , Vasconcelos Vasco T.
Published: December 2016

Session types describe structured communication on heterogeneously typed channels at a high level. Their tail-recursive structure imposes a protocol that can be described by a regular language. The types of transmitted values are drawn from the underlying functional language, abstracting from the details of serializing values of structured data types.

Context-free session types extend session types by allowing nested protocols that are not restricted to tail recursion. Nested protocols correspond to deterministic context-free languages. Such protocols are interesting in their own right, but they are particularly suited to describe the low-level serialization of tree-structured data in a type-safe way.

We establish the metatheory of context-free session types, prove that they properly generalize standard (two-party) session types, and take first steps towards type checking by showing that type equivalence is decidable.
Partial type equivalences for verified dependent interoperability
Authors: Dagand Pierre-Evariste , Tabareau Nicolas , Tanter Éric
Published: December 2016

Full-spectrum dependent types promise to enable the development of correct-by-construction software. However, even certified software needs to interact with simply-typed or untyped programs, be it to perform system calls, or to use legacy libraries. Trading static guarantees for runtime checks, the dependent interoperability framework provides a mechanism by which simply-typed values can safely be coerced to dependent types and, conversely, dependently-typed programs can defensively be exported to a simply-typed application. In this paper, we give a semantic account of dependent interoperability. Our presentation relies on and is guided by a pervading notion of type equivalence, whose importance has been emphasized in recent work on homotopy type theory. Specifically, we develop the notion of partial type equivalences as a key foundation for dependent interoperability. Our framework is developed in Coq; it is thus constructive and verified in the strictest sense of the terms. Using our library, users can specify domain-specific partial equivalences between data structures. Our library then takes care of the (sometimes, heavy) lifting that leads to interoperable programs. It thus becomes possible, as we shall illustrate, to internalize and hand-tune the extraction of dependently-typed programs to interoperable OCaml programs within Coq itself.
Constructive Galois connections: taming the Galois connection framework for mechanized metatheory
Authors: Darais David , Van Horn David
Published: December 2016

Galois connections are a foundational tool for structuring abstraction in semantics and their use lies at the heart of the theory of abstract interpretation. Yet, mechanization of Galois connections remains limited to restricted modes of use, preventing their general application in mechanized metatheory and certified programming.

This paper presents constructive Galois connections, a variant of Galois connections that is effective both on paper and in proof assistants; is complete with respect to a large subset of classical Galois connections; and enables more general reasoning principles, including the "calculational" style advocated by Cousot.

To design constructive Galois connection we identify a restricted mode of use of classical ones which is both general and amenable to mechanization in dependently-typed functional programming languages. Crucial to our metatheory is the addition of monadic structure to Galois connections to control a "specification effect". Effectful calculations may reason classically, while pure calculations have extractable computational content. Explicitly moving between the worlds of specification and implementation is enabled by our metatheory.

To validate our approach, we provide two case studies in mechanizing existing proofs from the literature: one uses calculational abstract interpretation to design a static analyzer, the other forms a semantic basis for gradual typing. Both mechanized proofs closely follow their original paper-and-pencil counterparts, employ reasoning principles not captured by previous mechanization approaches, support the extraction of verified algorithms, and are novel.
An abstract memory functor for verified C static analyzers
Authors: Blazy Sandrine , Laporte Vincent , Pichardie David
Published: December 2016

Abstract interpretation provides advanced techniques to infer numerical invariants on programs. There is an abundant literature about numerical abstract domains that operate on scalar variables. This work deals with lifting these techniques to a realistic C memory model. We present an abstract memory functor that takes as argument any standard numerical abstract domain, and builds a memory abstract domain that finely tracks properties about memory contents, taking into account union types, pointer arithmetic and type casts. This functor is implemented and verified inside the Coq proof assistant with respect to the CompCert compiler memory model. Using the Coq extraction mechanism, it is fully executable and used by the Verasco C static analyzer.
Fully abstract compilation via universal embedding
Authors: New Max S. , Bowman William J. , Ahmed Amal
Published: December 2016

A
fully abstract
compiler guarantees that two source components are observationally equivalent in the source language if and only if their translations are observationally equivalent in the target. Full abstraction implies the translation is
secure
: target-language attackers can make no more observations of a compiled component than a source-language attacker interacting with the original source component. Proving full abstraction for realistic compilers is challenging because realistic target languages contain features (such as control effects) unavailable in the source, while proofs of full abstraction require showing that every target context to which a compiled component may be linked can be
back-translated
to a behaviorally equivalent source context.

We prove the first full abstraction result for a translation whose target language contains exceptions, but the source does not. Our translation---specifically, closure conversion of simply typed λ-calculus with recursive types---uses types at the target level to ensure that a compiled component is never linked with attackers that have more distinguishing power than source-level attackers. We present a new back-translation technique based on a shallow embedding of the target language into the source language at a dynamic type. Then boundaries are inserted that mediate terms between the untyped embedding and the strongly-typed source. This technique allows back-translating non-terminating programs, target features that are untypeable in the source, and well-bracketed effects.
A fully concurrent garbage collector for functional programs on multicore processors
Authors: Ueno Katsuhiro , Ohori Atsushi
Published: December 2016

This paper presents a concurrent garbage collection method for functional programs running on a multicore processor. It is a concurrent extension of our bitmap-marking non-moving collector with Yuasa's snapshot-at-the-beginning strategy. Our collector is unobtrusive in the sense of the Doligez-Leroy-Gonthier collector; the collector does not stop any mutator thread nor does it force them to synchronize globally. The only critical sections between a mutator and the collector are the code to enqueue/dequeue a 32 kB allocation segment to/from a global segment list and the write barrier code to push an object pointer onto the collector's stack. Most of these data structures can be implemented in standard lock-free data structures. This achieves both efficient allocation and unobtrusive collection in a multicore system. The proposed method has been implemented in SML#, a full-scale Standard ML compiler supporting multiple native threads on multicore CPUs. Our benchmark tests show a drastically short pause time with reasonably low overhead compared to the sequential bitmap-marking collector.
A type theory for incremental computational complexity with control flow changes
Authors: Çiçek Ezgi , Paraskevopoulou Zoe , Garg Deepak
Published: December 2016

Incremental computation aims to speed up re-runs of a program after its inputs have been modified slightly. It works by recording a trace of the program's first run and propagating changes through the trace in incremental runs, trying to re-use as much of the original trace as possible. The recent work CostIt is a type and effect system to establish the time complexity of incremental runs of a program, as a function of input changes. However, CostIt is limited in two ways. First, it prohibits input changes that influence control flow. This makes it impossible to type programs that, for instance, branch on inputs that may change. Second, the soundness of CostIt is proved relative to an abstract cost semantics, but it is unclear how the semantics can be realized.

In this paper, we address both these limitations. We present DuCostIt, a re-design of CostIt, that combines reasoning about costs of change propagation and costs of from-scratch evaluation. The latter lifts the restriction on control flow changes. To obtain the type system, we refine Flow Caml, a type system for information flow analysis, with cost effects. Additionally, we inherit from CostIt index refinements to track data structure sizes and a co-monadic type. Using a combination of binary and unary step-indexed logical relations, we prove DuCostIt's cost analysis sound relative to not only an abstract cost semantics, but also a concrete semantics, which is obtained by translation to an ML-like language.
TensorFlow: learning functions at scale
Authors: Abadi Martín
Published: December 2016

TensorFlow is a machine learning system that operates at large scale and in heterogeneous environments. Its computational model is based on dataflow graphs with mutable state. Graph nodes may be mapped to different machines in a cluster, and within each machine to CPUs, GPUs, and other devices. TensorFlow supports a variety of applications, but it particularly targets training and inference with deep neural networks. It serves as a platform for research and for deploying machine learning systems across many areas, such as speech recognition, computer vision, robotics, information retrieval, and natural language processing. In this talk, we describe TensorFlow and outline some of its applications. We also discuss the question of what TensorFlow and deep learning may have to do with functional programming. Although TensorFlow is not purely functional, many of its uses are concerned with optimizing functions (during training), then with applying those functions (during inference). These functions are defined as compositions of simple primitives (as is common in functional programming), with internal data representations that are learned rather than manually designed. TensorFlow is joint work with many other people in the Google Brain team and elsewhere. More information is available at tensorflow.org.
Journey to find bugs in JavaScript web applications in the wild
Authors: Ryu Sukyoung
Published: December 2016

Analyzing real-world JavaScript web applications is a challenging task. On top of understanding the semantics of JavaScript, it requires modeling of web documents, platform objects, and interactions between them. Not only the JavaScript language itself but also its usage patterns are extremely dynamic. JavaScript can generate code and run it during evaluation, and most web applications load JavaScript code dynamically. Such dynamic characteristics of JavaScript web applications make pure static analysis approaches inapplicable. In this talk, we present our attempts to analyze JavaScript web applications in the wild mostly statically using various approaches. From pure JavaScript programs to JavaScript web applications using platform-specific libraries and dynamic code loading, we explain technical challenges in analyzing each of them and how we built an open-source analysis framework for JavaScript, SAFE, that addresses the challenges incrementally. In spite of active research accomplishments in analysis of JavaScript web applications, many issues still remain to be resolved such as events, callback functions, and hybrid web applications. We discuss possible future research directions and open challenges.
Chain: tasks and channels for reliable intermittent programs
Authors: Colin Alexei , Lucia Brandon
Published: December 2016

Energy harvesting computers enable general-purpose computing using energy collected from their environment. Energy-autonomy of such devices has great potential, but their intermittent power supply poses a challenge. Intermittent program execution compromises progress and leaves state inconsistent. This work describes Chain: a new model for programming intermittent devices.

A Chain program is a set of programmer-defined tasks that compute and exchange data through channels. Chain guarantees forward progress at task granularity. A task is restartable and never sees inconsistent state, because its input and output channels are separated. Our system supports language features for expressing advanced data exchange patterns and for encapsulating reusable functionality.

Chain fundamentally differs from state-of-the-art checkpointing approaches and does not incur the associated overhead. We implement Chain as C language extensions and a runtime library. We used Chain to implement four applications: machine learning, encryption, compression, and sensing. In experiments, Chain ensured consistency where prior approaches failed and improved throughput by 2-7x over the leading state-of-the-art system.
Dynamically diagnosing type errors in unsafe code
Authors: Kell Stephen
Published: December 2016

Existing approaches for detecting type errors in unsafe languages are limited. Static analysis methods are imprecise, and often require source-level changes, while most dynamic methods check only memory properties (bounds, liveness, etc.), owing to a lack of run-time type information. This paper describes libcrunch, a system for binary-compatible run-time type checking of unmodified unsafe code, currently focusing on C. Practical experience shows that our prototype implementation is easily applicable to many real codebases without source-level modification, correctly flags programmer errors with a very low rate of false positives, offers a very low run-time overhead, and covers classes of error caught by no previously existing tool.
Asserting reliable convergence for configuration management scripts
Authors: Hanappi Oliver , Hummer Waldemar , Dustdar Schahram
Published: December 2016

The rise of elastically scaling applications that frequently deploy new machines has led to the adoption of DevOps practices across the cloud engineering stack. So-called configuration management tools utilize scripts that are based on declarative resource descriptions and make the system converge to the desired state. It is crucial for convergent configurations to be able to gracefully handle transient faults, e.g., network outages when downloading and installing software packages. In this paper we introduce a conceptual framework for asserting reliable convergence in configuration management. Based on a formal definition of configuration scripts and their resources, we utilize state transition graphs to test whether a script makes the system converge to the desired state under different conditions. In our generalized model, configuration actions are partially ordered, often resulting in prohibitively many possible execution orders. To reduce this problem space, we define and analyze a property called preservation, and we show that if preservation holds for all pairs of resources, then convergence holds for the entire configuration. Our implementation builds on Puppet, but the approach is equally applicable to other frameworks like Chef, Ansible, etc. We perform a comprehensive evaluation based on real world Puppet scripts and show the effectiveness of the approach. Our tool is able to detect all idempotence and convergence related issues in a set of existing Puppet scripts with known issues as well as some hitherto undiscovered bugs in a large random sample of scripts.
Automatic enforcement of expressive security policies using enclaves
Authors: Gollamudi Anitha , Chong Stephen
Published: December 2016

Hardware-based enclave protection mechanisms, such as Intel's SGX, ARM's TrustZone, and Apple's Secure Enclave, can protect code and data from powerful low-level attackers. In this work, we use enclaves to enforce strong application-specific information security policies.

We present
IMP

E

, a novel calculus that captures the essence of SGX-like enclave mechanisms, and show that a security-type system for
IMP

E

can enforce expressive confidentiality policies (including erasure policies and delimited release policies) against powerful low-level attackers, including attackers that can arbitrarily corrupt non-enclave code, and, under some circumstances, corrupt enclave code. We present a translation from an expressive security-typed calculus (that is not aware of enclaves) to
IMP

E

. The translation automatically places code and data into enclaves to enforce the security policies of the source program.
Java and scala's type systems are unsound: the existential crisis of null pointers
Authors: Amin Nada , Tate Ross
Published: December 2016

We present short programs that demonstrate the unsoundness of Java and Scala's current type systems. In particular, these programs provide parametrically polymorphic functions that can turn any type into any type without (down)casting. Fortunately, parametric polymorphism was not integrated into the Java Virtual Machine (JVM), so these examples do not demonstrate any unsoundness of the JVM. Nonetheless, we discuss broader implications of these findings on the field of programming languages.
Low-overhead and fully automated statistical debugging with abstraction refinement
Authors: Zuo Zhiqiang , Fang Lu , Khoo Siau-Cheng , Xu Guoqing , Lu Shan
Published: December 2016

Cooperative statistical debugging is an effective approach for diagnosing production-run failures. To quickly identify failure predictors from the huge program predicate space, existing techniques rely on random or heuristics-guided predicate sampling at the user side. However, none of them can satisfy the requirements of low cost, low diagnosis latency, and high diagnosis quality simultaneously, which are all indispensable for statistical debugging to be practical.

This paper presents a new technique that tackles the above challenges. We formulate the technique as an instance of abstraction refinement, where efficient abstract-level profiling is first applied to the whole program and its execution brings information that can pinpoint suspicious coarse-grained entities that need to be refined. The refinement profiles a corresponding set of fine-grained entities, and generates feedback that determines what to prune and what to refine next. The process is fully automated, and more importantly, guided by a mathematically rigorous analysis that guarantees that our approach produces the same debugging results as an exhaustive analysis in deterministic settings.

We have implemented this technique for both C and Java on both single machine and distributed system. A thorough evaluation demonstrates that our approach yields (1) an order of magnitude reduction in the user-side runtime overhead even compared to a sampling-based approach and (2) two orders of magnitude reduction in the size of data transferred over the network, completely automatically without sacrificing any debugging capability.
Gentrification gone too far? affordable 2nd-class values for fun and (co-)effect
Authors: Osvald Leo , Essertel Grégory , Wu Xilun , Alayón Lilliam I. González , Rompf Tiark
Published: December 2016

First-class functions dramatically increase expressiveness, at the expense of static guarantees. In ALGOL or PASCAL, functions could be passed as arguments but never escape their defining scope. Therefore, function arguments could serve as temporary access tokens or capabilities, enabling callees to perform some action, but only for the duration of the call. In modern languages, such programming patterns are no longer available.

The central thrust of this paper is to re-introduce second-class functions and other values alongside first-class entities in modern languages. We formalize second-class values with stack-bounded lifetimes as an extension to simply-typed λ calculus, and for richer type systems such as F
<:
and systems with path-dependent types. We generalize the binary first- vs second-class distinction to arbitrary privilege lattices, with the underlying type lattice as a special case. In this setting, abstract types naturally enable privilege parametricity. We prove type soundness and lifetime properties in Coq.

We implement our system as an extension of Scala, and present several case studies. First, we modify the Scala Collections library and add privilege annotations to all higher-order functions. Privilege parametricity is key to retain the high degree of code-reuse between sequential and parallel as well as lazy and eager collections. Second, we use scoped capabilities to introduce a model of checked exceptions in the Scala library, with only few changes to the code. Third, we employ second-class capabilities for memory safety in a region-based off-heap memory library.
A compiler for throughput optimization of graph algorithms on GPUs
Authors: Pai Sreepathi , Pingali Keshav
Published: December 2016

Writing high-performance GPU implementations of graph algorithms can be challenging. In this paper, we argue that three optimizations called throughput optimizations are key to high-performance for this application class. These optimizations describe a large implementation space making it unrealistic for programmers to implement them by hand.

To address this problem, we have implemented these optimizations in a compiler that produces CUDA code from an intermediate-level program representation called IrGL. Compared to state-of-the-art handwritten CUDA implementations of eight graph applications, code generated by the IrGL compiler is up to 5.95x times faster (median 1.4x) for five applications and never more than 30% slower for the others. Throughput optimizations contribute an improvement up to 4.16x (median 1.4x) to the performance of unoptimized IrGL code.
Extensible access control with authorization contracts
Authors: Moore Scott , Dimoulas Christos , Findler Robert Bruce , Flatt Matthew , Chong Stephen
Published: December 2016

Existing programming language access control frameworks do not meet the needs of all software components. We propose an expressive framework for implementing access control monitors for components. The basis of the framework is a novel concept: the authority environment. An authority environment associates rights with an execution context. The building blocks of access control monitors in our framework are authorization contracts: software contracts that manage authority environments. We demonstrate the expressiveness of our framework by implementing a diverse set of existing access control mechanisms and writing custom access control monitors for three realistic case studies.
Semantics-based program verifiers for all languages
Authors: Stefănescu Andrei , Park Daejun , Yuwen Shijiao , Li Yilong , Roşu Grigore
Published: December 2016

We present a language-independent verification framework that can be instantiated with an operational semantics to automatically generate a program verifier. The framework treats both the operational semantics and the program correctness specifications as reachability rules between matching logic patterns, and uses the sound and relatively complete reachability logic proof system to prove the specifications using the semantics. We instantiate the framework with the semantics of one academic language, KernelC, as well as with three recent semantics of real-world languages, C, Java, and JavaScript, developed independently of our verification infrastructure. We evaluate our approach empirically and show that the generated program verifiers can check automatically the full functional correctness of challenging heap-manipulating programs implementing operations on list and tree data structures, like AVL trees. This is the first approach that can turn the operational semantics of real-world languages into correct-by-construction automatic verifiers.
Prioritized garbage collection: explicit GC support for software caches
Authors: Nunez Diogenes , Guyer Samuel Z. , Berger Emery D.
Published: December 2016

Programmers routinely trade space for time to increase performance, often in the form of caching or memoization. In managed languages like Java or JavaScript, however, this space-time tradeoff is complex. Using more space translates into higher garbage collection costs, especially at the limit of available memory. Existing runtime systems provide limited support for space-sensitive algorithms, forcing programmers into difficult and often brittle choices about provisioning.

This paper presents
prioritized garbage collection
, a cooperative programming language and runtime solution to this problem. Prioritized GC provides an interface similar to soft references, called
priority references
, which identify objects that the collector can reclaim eagerly if necessary. The key difference is an API for defining the policy that governs when priority references are cleared and in what order. Application code specifies a priority value for each reference and a target memory bound. The collector reclaims references, lowest priority first, until the total memory footprint of the cache fits within the bound. We use this API to implement a space-aware least-recently-used (LRU) cache, called a
Sache
, that is a drop-in replacement for existing caches, such as Google's Guava library. The garbage collector automatically grows and shrinks the Sache in response to available memory and workload with minimal provisioning information from the programmer. Using a Sache, it is almost impossible for an application to experience a memory leak, memory pressure, or an out-of-memory crash caused by software caching.
Hybrid STM/HTM for nested transactions on OpenJDK
Authors: Chapman Keith , Hosking Antony L. , Moss J. Eliot B.
Published: December 2016

Transactional memory (TM) has long been advocated as a promising pathway to more automated concurrency control for scaling concurrent programs running on parallel hardware. Software TM (STM) has the benefit of being able to run general transactional programs, but at the significant cost of overheads imposed to log memory accesses, mediate access conflicts, and maintain other transaction metadata. Recently, hardware manufacturers have begun to offer commodity hardware TM (HTM) support in their processors wherein the transaction metadata is maintained "for free" in hardware. However, HTM approaches are only
best-effort
: they cannot successfully run all transactional programs, whether because of hardware capacity issues (causing large transactions to fail), or compatibility restrictions on the processor instructions permitted within hardware transactions (causing transactions that execute those instructions to fail). In such cases, programs must include failure-handling code to attempt the computation by some other software means, since retrying the transaction would be futile. Thus, a canonical use of HTM is
lock elision
: replacing lock regions with transactions, retrying some number of times in the case of conflicts, but falling back to locking when HTM fails for other reasons.

Here, we describe how software and hardware schemes can combine seamlessly into a hybrid system in support of transactional programs, allowing use of low-cost HTM when it works, but reverting to STM when it doesn't. We describe heuristics used to make this choice dynamically and automatically, but allowing the transition back to HTM opportunistically. Our implementation is for an extension of Java having syntax for both open and closed nested transactions, and boosting, running on the OpenJDK, with dynamic injection of STM mechanisms (into code variants used under STM) and HTM instructions (into code variants used under HTM). Both schemes are compatible to allow different threads to run concurrently with either mechanism, while preserving transaction safety. Using a standard synthetic benchmark we demonstrate that HTM offers significant acceleration of both closed and open nested transactions, while yielding parallel scaling up to the limits of the hardware, whereupon scaling in software continues but with the penalty to throughput imposed by software mechanisms.
Portable inter-workgroup barrier synchronisation for GPUs
Authors: Sorensen Tyler , Donaldson Alastair F. , Batty Mark , Gopalakrishnan Ganesh , Rakamarić Zvonimir
Published: December 2016

Despite the growing popularity of GPGPU programming, there is not yet a portable and formally-specified barrier that one can use to synchronise across workgroups. Moreover, the occupancy-bound execution model of GPUs breaks assumptions inherent in traditional software execution barriers, exposing them to deadlock. We present an occupancy discovery protocol that dynamically discovers a safe estimate of the occupancy for a given GPU and kernel, allowing for a starvation-free (and hence, deadlock-free) inter-workgroup barrier by restricting the number of workgroups according to this estimate. We implement this idea by adapting an existing, previously non-portable, GPU inter-workgroup barrier to use OpenCL 2.0 atomic operations, and prove that the barrier meets its natural specification in terms of synchronisation.

We assess the portability of our approach over eight GPUs spanning four vendors, comparing the performance of our method against alternative methods. Our key findings include: (1) the recall of our discovery protocol is nearly 100%; (2) runtime comparisons vary substantially across GPUs and applications; and (3) our method provides portable and safe inter-workgroup synchronisation across the applications we study.
Incremental forest: a DSL for efficiently managing filestores
Authors: DiLorenzo Jonathan , Zhang Richard , Menzies Erin , Fisher Kathleen , Foster Nate
Published: December 2016

File systems are often used to store persistent application data, but manipulating file systems using standard APIs can be difficult for programmers. Forest is a domain-specific language that bridges the gap between the on-disk and in-memory representations of file system data. Given a high-level specification of the structure, contents, and properties of a collection of directories, files, and symbolic links, the Forest compiler generates tools for loading, storing, and validating that data. Unfortunately, the initial implementation of Forest offered few mechanisms for controlling cost-e.g., the run-time system could load gigabytes of data, even if only a few bytes were needed. This paper introduces Incremental Forest (iForest), an extension to Forest with an explicit
delay
construct that programmers can use to precisely control costs. We describe the design of iForest using a series of running examples, present a formal semantics in a core calculus, and define a simple cost model that accurately characterizes the resources needed to use a given specification. We propose
skins
, which allow programmers to modify the delay structure of a specification in a compositional way, and develop a static type system for ensuring compatibility between specifications and skins. We prove the soundness and completeness of the type system and a variety of algebraic properties of skins. We describe an OCaml implementation and evaluate its performance on applications developed in collaboration with watershed hydrologists.
Automatic parallelization of pure method calls via conditional future synthesis
Authors: Surendran Rishi , Sarkar Vivek
Published: December 2016

We introduce a novel approach for using futures to automatically parallelize the execution of pure method calls. Our approach is built on three new techniques to address the challenge of automatic parallelization via future synthesis: candidate future synthesis, parallelism benefit analysis, and threshold expression synthesis. During
candidate future synthesis
, our system annotates pure method calls as async expressions and synthesizes a parallel program with future objects and their type declarations. Next, the system performs a
parallel benefit analysis
to determine which async expressions may need to be executed sequentially due to overhead reasons, based on execution profile information collected from multiple test inputs. Finally,
threshold expression synthesis
uses the output from parallelism benefit analysis to synthesize predicate expressions that can be used to determine at runtime if a specific pure method call should be executed sequentially or in parallel.

We have implemented our approach, and the results obtained from an experimental evaluation of the complete system on a range of sequential Java benchmarks are very encouraging. Our evaluation shows that our approach can provide significant parallel speedups of up to 7.4x (geometric mean of 3.69x) relative to the sequential programs when using 8 processor cores, with zero programmer effort beyond providing the sequential program and test cases for parallelism benefit analysis.
Finding compiler bugs via live code mutation
Authors: Sun Chengnian , Le Vu , Su Zhendong
Published: December 2016

Validating optimizing compilers is challenging because it is hard to generate valid test programs (i.e., those that do not expose any undefined behavior). Equivalence Modulo Inputs (EMI) is an effective, promising methodology to tackle this problem. Given a test program with some inputs, EMI mutates the program to derive variants that are semantically equivalent w.r.t. these inputs. The state-of-the-art instantiations of EMI are Orion and Athena, both of which rely on deleting code from or inserting code into code regions that are not executed under the inputs. Although both have demonstrated their ability in finding many bugs in GCC and LLVM, they are still limited due to their mutation strategies that operate only on dead code regions.

This paper presents a novel EMI technique that allows mutation in the entire program (i.e., both live and dead regions). By removing the restriction of mutating only the dead regions, our technique significantly increases the EMI variant space. It also helps to more thoroughly stress test compilers as compilers must optimize mutated live code, whereas mutated dead code might be eliminated. Finally, our technique also makes compiler bugs more noticeable as miscompilations on mutated dead code may not be observable.

We have realized the proposed technique in Hermes. The evaluation demonstrates Hermes’s effectiveness. In 13 months, Hermes found 168 confirmed, valid bugs in GCC and LLVM, of which 132 have already been fixed.
Dynamin-related protein 1 mediates low glucose-induced endothelial dysfunction in human arterioles
Authors: Tanner Michael J. , Wang Jingli , Ying Rong , Suboc Tisha B. , Malik Mobin , Couillard Allison , Branum Amberly , Puppala Venkata , Widlansky Michael E.
Published: December 2016

Intensive glycemic regulation has resulted in an increased incidence of hypoglycemia. Hypoglycemic burden correlates with adverse cardiovascular complications and contributes acutely and chronically to endothelial dysfunction. Prior data indicate that mitochondrial dysfunction contributes to hypoglycemia-induced endothelial dysfunction, but the mechanisms behind this linkage remain unknown. We attempt to determine whether clinically relevant low-glucose (LG) exposures acutely induce endothelial dysfunction through activation of the mitochondrial fission process. Characterization of mitochondrial morphology was carried out in cultured endothelial cells by using confocal microscopy. Isolated human arterioles were used to explore the effect LG-induced mitochondrial fission has on the formation of detrimental reactive oxygen species (ROS), bioavailability of nitric oxide (NO), and endothelial-dependent vascular relaxation. Fluorescence microscopy was employed to visualize changes in mitochondrial ROS and NO levels and videomicroscopy applied to measure vasodilation response. Pharmacological disruption of the profission protein Drp1 with Mdivi-1 during LG exposure reduced mitochondrial fragmentation among vascular endothelial cells (LG: 0.469; LG+Mdivi-1: 0.276; P = 0.003), prevented formation of vascular ROS (LG: 2.036; LG+Mdivi-1: 1.774; P = 0.005), increased the presence of NO (LG: 1.352; LG+Mdivi-1: 1.502; P = 0.048), and improved vascular dilation response to acetylcholine (LG: 31.6%; LG+Mdivi-1; 78.5% at maximum dose; P < 0.001). Additionally, decreased expression of Drp1 via siRNA knockdown during LG conditions also improved vascular relaxation. Exposure to LG imparts endothelial dysfunction coupled with altered mitochondrial phenotypes among isolated human arterioles. Disruption of Drp1 and subsequent mitochondrial fragmentation events prevents impaired vascular dilation, restores mitochondrial phenotype, and implicates mitochondrial fission as a primary mediator of LG-induced endothelial dysfunction.

NEW & NOTEWORTHY Acute low-glucose exposure induces mitochondrial fragmentation in endothelial cells via Drp1 and is associated with impaired endothelial function in human arterioles. Targeting of Drp1 prevents fragmentation, improves vasofunction, and may provide a therapeutic target for improving cardiovascular complications among diabetics.

Listen to this article’s corresponding podcast @ http://ajpheart.podbean.com/e/mitochondrial-dynamics-impact-endothelial-function/ .