bluuebunny/crossref_metadata_2025 huggingface dataset:
Efficient runtime tracking of allocation sites in Java
Authors: Odaira Rei , Ogata Kazunori , Kawachiya Kiyokuni , Onodera Tamiya , Nakatani Toshio
Published: April 2020

Tracking the allocation site of every object at runtime is useful for reliable, optimized Java. To be used in production environments, the tracking must be accurate with minimal speed loss. Previous approaches suffer from performance degradation due to the additional field added to each object or track the allocation sites only probabilistically. We propose two novel approaches to track the allocation sites of every object in Java with only a 1.0% slow-down on average. Our first approach, the
Allocation-Site-as-a-Hash-code (ASH) Tracker
, encodes the allocation site ID of an object into the hash code field of its header by regarding the ID as part of the hash code. ASH Tracker avoids an excessive increase in hash code collisions by dynamically shrinking the bit-length of the ID as more and more objects are allocated at that site. For those Java VMs without the hash code field, our second approach, the
Allocation-Site-via-a-Class-pointer (ASC) Tracker
, makes the class pointer field in an object header refer to the allocation site structure of the object, which in turn points to the actual class structure. ASC Tracker mitigates the indirection overhead by constant-class-field duplication and allocation-site equality checks. While a previous approach of adding a 4-byte field caused up to 14.4% and an average 5% slowdown, both ASH and ASC Trackers incur at most a 2.0% and an average 1.0% loss. We demonstrate the usefulness of our low-overhead trackers by an allocation-site-aware memory leak detector and allocation-site-based pretenuring in generational GC. Our pretenuring achieved on average 1.8% and up to 11.8% speedups in SPECjvm2008.
Dynamic binary translation specialized for embedded systems
Authors: Kondoh Goh , Komatsu Hideaki
Published: April 2020

This paper describes the design and implementation of a novel dynamic binary translation technique specialized for embedded systems. Virtual platforms have been widely used to develop embedded software and dynamic binary translation is essential to boost their speed in simulations. However, unlike application simulation, the code generated for systems simulation is still slow because the simulator must replicate all of the functions of the target hardware. Embedded systems, which focus on providing one or a few functions, utilize only a small portion of the processor's features most of the time. For example, they may use a Memory Management Unit (MMU) in a processor to map physical memory to effective addresses, but they may not need paged memory support as in an OS. We can exploit this to specialize the dynamically translated code for more performance.

We built a specialization framework on top of a functional simulator with a dynamic binary translator. Using the framework, we implemented three specializers for an MMU, bi-endianness, and register banks. Experiments with the EEMBC1.1 benchmark showed that the speed of the specialized code was up to 39% faster than the unspecialized code.
Feature interactions, products, and composition
Authors: Batory Don , Höfner Peter , Kim Jongwook
Published: April 2020

The relationship between feature modules and feature interactions is not well-understood. To explain classic examples of feature interaction, we show that features are not only composed sequentially, but also by cross-product and interaction operations that heretofore were implicit in the literature. Using the Colored IDE (CIDE) tool as our starting point, we (a) present a formal model of these operations, (b) show how it connects and explains previously unrelated results in
Feature Oriented Software Development (FOSD)
, and (c) describe a tool, based on our formalism, that demonstrates how changes in composed documents can be back-propagated to their original feature module definitions, thereby improving FOSD tooling.
On the impact of feature dependencies when maintaining preprocessor-based software product lines
Authors: Ribeiro Márcio , Queiroz Felipe , Borba Paulo , Tolêdo Társis , Brabrand Claus , Soares Sérgio
Published: April 2020

During Software Product Line (SPL) maintenance tasks, Virtual Separation of Concerns (VSoC) allows the programmer to focus on one feature and hide the others. However, since features depend on each other through variables and control-flow, feature modularization is compromised since the maintenance of one feature may break another. In this context,
emergent interfaces
can capture dependencies between the feature we are maintaining and the others, making developers aware of dependencies. To better understand the impact of code level feature dependencies during SPL maintenance, we have investigated the following two questions:
how often methods with preprocessor directives contain feature dependencies? How feature dependencies impact maintenance effort when using VSoC and emergent interfaces?
Answering the former is important for assessing how often we may face feature dependency problems. Answering the latter is important to better understand to what extent emergent interfaces complement VSoC during maintenance tasks. To answer them, we analyze 43 SPLs of different domains, size, and languages. The data we collect from them complement previous work on preprocessor usage. They reveal that the feature dependencies we consider in this paper are reasonably common in practice; and that emergent interfaces can reduce maintenance effort during the SPL maintenance tasks we regard here.
Generation of geometric programs specified by diagrams
Authors: Li Yulin , Novak Gordon S.
Published: April 2020

The GeoGram system [21]generates programs for geometric computations by combining generic software components as specified by diagrams constructed using a graphical interface. The user specifies known and desired quantities. As diagrams are constructed, the system maintains symbolic geometric facts describing the construction. Inferences based on the diagram are used to derive new facts and to introduce new objects based on geometric reasoning, to filter choices presented to the user, to interpret the user's intention in ambiguous cases, to detect over-specification, and to generate the program. A knowledge base of descriptions of generic software components is used to prove that features of the geometry can be computed from known values. These local proofs are combined to guide generation of a program that computes the desired values from inputs. The library of generic geometric program components is used to generate both in-line code and specialized subroutines; partial evaluation improves the efficiency of the generated code. The resulting program is automatically translated into the desired language. The program can also be run interactively to simulate the geometry by generating graphical traces on the diagram as input quantities are varied.
Generating database migrations for evolving web applications
Authors: Vermolen Sander Daniël , Wachsmuth Guido , Visser Eelco
Published: April 2020

WebDSL is a domain-specific language for the implementation of dynamic web applications with a rich data model. It provides developers with object-oriented data modeling concepts but abstracts over implementation details for persisting application data in relational databases. When the underlying data model of an application evolves, persisted application data has to be migrated. While implementing migration at the database level breaks the abstractions provided by WebDSL, an implementation at the data model level requires to intermingle migration with application code. In this paper, we present a domain-specific language for the coupled evolution of data models and application data. It allows to specify data model evolution as a separate concern at the data model level and can be compiled to migration code at the database level. Its linguistic integration with WebDSL enables static checks for evolution validity and correctness.
Helping programmers help users
Authors: Freeman John , Järvi Jaakko , Kim Wonseok , Marcus Mat , Parent Sean
Published: April 2020

User interfaces exhibit a wide range of features that are designed to assist users. Interaction with one widget may trigger value changes, disabling, or other behaviors in other widgets. Such automatic behavior may be confusing or disruptive to users. Research literature on user interfaces offers a number of solutions, including interface features for explaining or controlling these behaviors. To help programmers help users, the implementation costs of these features need to be much lower. Ideally, they could be generated for free. This paper shows how several help and control mechanisms can be implemented as algorithms and reused across interfaces, making the cost of their adoption negligible. Specifically, we describe generic help mechanisms for visualizing data flow and explaining command deactivation, and a mechanism for controlling the flow of data. A reusable implementation of these features is enabled by our property model framework, where the data manipulated through a user interface is modeled as a constraint system.
FORMLESS
Authors: Hashemi Matin , Foroozannejad Mohammad H. , Ghiasi Soheil , Etzel Christoph
Published: April 2020

Variants of dataflow specification models are widely used to synthesize streaming applications for distributed-memory parallel processors. We argue that current practice of specifying streaming applications using
rigid
dataflow models, implicitly prohibits a number of platform oriented optimizations and hence limits portability and scalability with respect to number of processors. We motivate
Functionally-cOnsistent stRucturally-MalLEabe Streaming Specification
, dubbed FORMLESS, which refers to raising the abstraction level beyond fixed-structure dataflow to address its portability and scalability limitations. To demonstrate the potential of the idea, we develop a design space exploration scheme to customize the application specification to better fit the target platform. Experiments with several common streaming case studies demonstrate improved portability and scalability over conventional dataflow specification models, and confirm the effectiveness of our approach.
Hi-Lite
Authors: Kanig Johannes , Schonberg Edmond , Dross Claire
Published: April 2020

Formal program verification tools check that a program correctly implements its specification. Existing specification languages for well-known programming languages (Ada, C, Java, C#) have been developed independently from the programming language to which they apply. As a result, specifications are expressed separately from the code, typically as stylized comments, and the verification tools often bear no direct relation to the production compiler. We argue that this approach is problematic, and that the compiler and the verification tools should be integrated seamlessly. Based on our current work on the Hi-Lite project to develop a formal verification tool for Ada2012, we show that in an integrated setting, the compiler becomes the centerpiece of the verification architecture, and supports both static proofs and run-time assertion checking. Such an environment does much to simplify software certification.
Implementation of a simple dimensionality checking system in Ada 2012
Authors: Schonberg Edmond , Pucci Vincent
Published: April 2020

We present the design and implementation of a dimensionality checking system in Ada 2012. The system is implemented in the GNAT compiler, and performs compile-time checks to verify the dimensional consistency of physical computations. The system allows the user to define his own system of units, and imposes no run-time changes nor multiple compilation passes on the user.
FAA's controller pilot automatic data communication (data comm) system software development
Authors: O'Leary Jeffrey , Srivastava Alok
Published: April 2020

To meet future demands and avoid gridlock in the sky and at airports, US Federal Aviation Administration's (FAA) NextGen Data Communications (DataComm) Program is designed to advance today's analog voice-only air-to-ground communications system to one in which digital communications become an alternate and eventually predominant mode of communication.
Package templates
Authors: Axelsen Eyvind W. , Krogdahl Stein
Published: April 2020

Package Templates (PT) is a mechanism designed for writing reusable modules, called templates, each consisting of a set of classes that can be adapted to their use in a program through compile-time specialization. A template must be
instantiated
in a program before its classes can be used. The mechanism supports type-safe renaming, merging, type parameterization and refinement in the form of static additions and overrides that are orthogonal to the corresponding concepts of ordinary inheritance.

In this paper, we consider PT as an extension to Java, and a PT program will then consist of a number of Java packages and templates, where templates are instantiated in packages or other templates. Our aim and main contribution is to define the meaning of such a program, and to show that this definition is consistent. We first show this for a core subset of PT, C-PT, and define a set of source-to-source transformations for converting C-PT programs to plain Java programs using semantics we have described informally in previous papers. We can then define the meaning of a C-PT program in terms of the resulting Java program. Thus, we have to verify that the transformations will always convert a legal C-PT program to a legal Java program. Finally, we briefly discuss how this approach can be extended to full PT.

A main challenge is to preserve externally visible names (for classes, methods and fields), and at the same time prevent unwanted subsequent rebindings caused e.g. by over-load resolution in the Java compiler. Names that are bound to declarations in a template should not be rebound to different declarations by subsequent compositions or adaptions.

In addition to defining the runtime semantics of PT constructs in terms of their translation to Java, the transformation rules can also be seen as a high-level approach to how a compiler for this language might be implemented.
A three-level component model in component based software development
Authors: Zhang Huaxi (Yulin) , Zhang Lei , Urtado Christelle , Vauttier Sylvain , Huchard Marianne
Published: April 2020

Component-based development promotes a software development process that focuses on component reuse. How to describe a desired component before searching in the repository? How to find an existing component that fulfills the required functionalities? How to capture the system personalization based on its constitutive components' customization? To answer these questions, this paper claims that components should be described using three different forms at three development stages: architecture specification, configuration and assembly. However, no architecture description language proposes such a detailed description for components that supports such a three step component-based development. This paper proposes a three-level Adl, named Dedal, that enables the explicit and separate definitions of component roles, component classes, and component instances.
HotDrink
Authors: Freeman John , Järvi Jaakko , Foust Gabriel
Published: April 2020

HotDrink is a JavaScript library for constructing forms, dialogs, and other common user interfaces for Web applications. With HotDrink, instead of writing event handlers, developers declare a "view-model" in JavaScript and a set of "bindings" between the view-model and the HTML elements comprising the view. These specifications tend to be small, but they are enough for HotDrink to provide a fully operational GUI with multi-way dataflows, enabling/disabling of values, activation/deactivation of commands, and data validation. HotDrink implements these rich behaviors, expected of high-quality user interfaces, as generic reusable algorithms. This paper/tool demonstration introduces developers to the HotDrink library by stepping through the construction of an example web application GUI.

The library is a concrete realization of our prior work on the "property models" approach to declarative GUI programming. To encourage adoption among developers, we have packaged the technology following established web programming conventions.
Pol
Authors: Bagheri Hamid , Sullivan Kevin
Published: April 2020

Developing applications that use complex
platforms
for functionalities such as authentication and messaging is hard. Model-driven engineering promises to help, but transformation systems are themselves hard to produce. We contribute a new approach using constraint-based synthesis of partial code frameworks that developers complete by hand
without the need for hand-coded transformation systems
. Rather, synthesis is driven by formal, partial specifications of target platforms and application architectures, and by design (code) fragments encoding application-specific platform us-age patterns. We present results of an early evaluation using the case study method to test hypotheses of feasibility and potential industrial utility, using a laboratory model of a nationwide health information network as a subject system.
A Prefetching Scheme Exploiting both Data Layout and Access History on Disk
Authors: Jiang Song , Ding Xiaoning , Xu Yuehai , Davis Kei
Published: April 2020

Prefetching is an important technique for improving effective hard disk performance. A prefetcher seeks to accurately predict which data will be requested and load it ahead of the arrival of the corresponding requests. Current disk prefetch policies in major operating systems track access patterns at the level of file abstraction. While this is useful for exploiting application-level access patterns, for two reasons file-level prefetching cannot realize the full performance improvements achievable by prefetching. First, certain prefetch opportunities can only be detected by knowing the data layout on disk, such as the contiguous layout of file metadata or data from multiple files. Second, nonsequential access of disk data (requiring disk head movement) is much slower than sequential access, and the performance penalty for mis-prefetching a randomly located block, relative to that of a sequential block, is correspondingly greater.

To overcome the inherent limitations of prefetching at logical file level, we propose to perform prefetching directly at the level of disk layout, and in a portable way. Our technique, called
DiskSeen
, is intended to be supplementary to, and to work synergistically with, any present file-level prefetch policies. DiskSeen tracks the locations and access times of disk blocks and, based on analysis of their temporal and spatial relationships, seeks to improve the sequentiality of disk accesses and overall prefetching performance. It also implements a mechanism to minimize mis-prefetching, on a per-application basis, to mitigate the corresponding performance penalty.

Our implementation of the DiskSeen scheme in the Linux 2.6 kernel shows that it can significantly improve the effectiveness of prefetching, reducing execution times by 20%--60% for microbenchmarks and real applications such as
grep
,
CVS
, and
TPC-H
. Even for workloads specifically designed to expose its weaknesses, DiskSeen incurs only minor performance loss.
Sea depth measurement with restricted floating sensors
Authors: Li Mo , Yang Zheng , Liu Yunhao
Published: April 2020

Sea depth monitoring is a critical task for ensuring safe operation of harbors. Traditional schemes largely rely on labor-intensive work and expensive hardware. This study explores the possibility of deploying networked sensors on the surface of the sea, measuring and reporting the sea depth of given areas. We propose a Restricted Floating Sensors (RFS) model in which sensor nodes are anchored to the sea bottom, floating within a restricted area. Distinguished from traditional stationary or mobile sensor networks, the RFS network consists of sensor nodes with restricted mobility. We construct the network model and elaborate the corresponding localization problem. We show that by locating such RFS sensors, the sea depth can be estimated without the help of any extra ranging devices. A prototype system with 25 Telos sensor nodes is deployed to validate this design. We also examine the efficiency and scalability of this design through large-scale simulations.
Design and evaluation of random linear network coding Accelerators on FPGAs
Authors: Kim Sunwoo , Jeong Won Seob , Ro Won W. , Gaudiot Jean-Luc
Published: April 2020

Network coding is a well-known technique used to enhance network throughput and reliability by applying special coding to data packets. One critical problem in practice, when using the random linear network coding technique, is the high computational overhead. More specifically, using this technique in embedded systems with low computational power might cause serious delays due to the complex Galois field operations and matrix handling. To this end, this article proposes a high-performance decoding logic for random linear network coding using field-programmable gate-array (FPGA) technology. We expect that the inherent reconfigurability of FPGAs will provide sufficient performance as well as programmability to cope with changes in the specification of the coding. The main design motivation was to improve the decoding delay by dividing and parallelizing the entire decoding process. Fast arithmetic operations are achieved by the proposed parallelized GF ALUs, which allow calculations with all the elements of a single row of a matrix to be performed concurrently. To improve the flexibility in the utilization of the FPGA components, two different decoding methods have been designed and compared. The performance of the proposed idea is evaluated by comparing with the performance of the decoding process executed by general-purpose processors through an equivalent software algorithm. Overall, a maximum throughput of 65.98 Mbps is achieved with the proposed FPGA design on an XC5VLX110T Virtex 5 device. In addition, the proposed design provides speedups of up to 13.84 compared to an aggressively parallelized software decoding algorithm run on a quad-core AMD processor. Moreover, the design affords 12 times higher power efficiency in terms of throughput per watt than an ARM Coretex-A9 processor.
Names for free
Authors: Bernardy Jean-Philippe , Pouillard Nicolas
Published: April 2020

We propose a novel technique to represent names and binders in Haskell. The dynamic (run-time) representation is based on de Bruijn indices, but it features an interface to write and manipulate variables conviently, using Haskell-level lambdas and variables. The key idea is to use rich types: a subterm with an additional free variable is viewed either as forallν.ν → Term(ɑ + ν) or ϶ν.ν x Term(ν.ν) depending on whether it is constructed or analysed. We demonstrate on a number of examples how this approach permits to express term construction and manipulation in a natural way, while retaining the good properties of representations based on de Bruijn indices.
Data flow fusion with series expressions in Haskell
Authors: Lippmeier Ben , Chakravarty Manuel M.T. , Keller Gabriele , Robinson Amos
Published: April 2020

Existing approaches to array fusion can deal with straight-line producer consumer pipelines, but cannot fuse branching data flows where a generated array is consumed by several different consumers. Branching data flows are common and natural to write, but a lack of fusion leads to the creation of an intermediate array at every branch point. We present a new array fusion system that handles branches, based on Waters's series expression framework, but extended to work in a functional setting. Our system also solves a related problem in stream fusion, namely the introduction of duplicate loop counters. We demonstrate speedup over existing fusion systems for several key examples.
Causality of optimized Haskell
Authors: Wortmann Peter M. , Duke David
Published: April 2020

Profiling real-world Haskell programs is hard, as compiler optimizations make it tricky to establish causality between the source code and program behavior. In this paper we attack the root issue by performing a causality analysis of functional programs under optimization. We apply our findings to build a novel profiling infrastructure on top of the Glasgow Haskell Compiler, allowing for performance analysis even of aggressively optimized programs.
A verified information-flow architecture
Authors: Azevedo de Amorim Arthur , Collins Nathan , DeHon André , Demange Delphine , Hriţcu Cătălin , Pichardie David , Pierce Benjamin C. , Pollack Randy , Tolmach Andrew
Published: April 2020

SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with efficient and flexible propagation and combination of tags as instructions are executed. The operating system virtualizes these generic facilities to present an information-flow abstract machine that allows user programs to label sensitive data with rich confidentiality policies. We present a formal, machine-checked model of the key hardware and software mechanisms used to control information flow in SAFE and an end-to-end proof of noninterference for this model.
Abstract acceleration of general linear loops
Authors: Jeannet Bertrand , Schrammel Peter , Sankaranarayanan Sriram
Published: April 2020

We present abstract acceleration techniques for computing loop invariants for numerical programs with linear assignments and conditionals. Whereas abstract interpretation techniques typically over-approximate the set of reachable states iteratively, abstract acceleration captures the effect of the loop with a single, non-iterative transfer function applied to the initial states at the loop head. In contrast to previous acceleration techniques, our approach applies to any linear loop without restrictions. Its novelty lies in the use of the
Jordan normal form
decomposition of the loop body to derive symbolic expressions for the entries of the matrix modeling the effect of η ≥ Ο iterations of the loop. The entries of such a matrix depend on η through complex polynomial, exponential and trigonometric functions. Therefore, we introduces an
abstract domain for matrices
that captures the linear inequality relations between these complex expressions. This results in an abstract matrix for describing the fixpoint semantics of the loop.

Our approach integrates smoothly into standard abstract interpreters and can handle programs with nested loops and loops containing conditional branches. We evaluate it over small but complex loops that are commonly found in control software, comparing it with other tools for computing linear loop invariants. The loops in our benchmarks typically exhibit polynomial, exponential and oscillatory behaviors that present challenges to existing approaches. Our approach finds non-trivial invariants to prove useful bounds on the values of variables for such loops, clearly outperforming the existing approaches in terms of precision while exhibiting good performance.
Optimal dynamic partial order reduction
Authors: Abdulla Parosh , Aronis Stavros , Jonsson Bengt , Sagonas Konstantinos
Published: April 2020

Stateless model checking is a powerful technique for program verification, which however suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is Dynamic Partial Order Reduction (DPOR). We present a new DPOR algorithm, which is the first to be provably optimal in that it always explores the minimal number of executions. It is based on a novel class of sets, called
source sets
, which replace the role of persistent sets in previous algorithms. First, we show how to modify an existing DPOR algorithm to work with source sets, resulting in an efficient and simple to implement algorithm. Second, we extend this algorithm with a novel mechanism, called
wakeup trees
, that allows to achieve optimality. We have implemented both algorithms in a stateless model checking tool for Erlang programs. Experiments show that source sets significantly increase the performance and that wakeup trees incur only a small overhead in both time and space.
Proof search for propositional abstract separation logics via labelled sequents
Authors: Hóu Zhé , Clouston Ranald , Goré Rajeev , Tiu Alwen
Published: April 2020

Abstract separation logics are a family of extensions of Hoare logic for reasoning about programs that mutate memory. These logics are "abstract" because they are independent of any particular concrete memory model. Their assertion languages, called propositional abstract separation logics, extend the logic of (Boolean) Bunched Implications (BBI) in various ways.

We develop a modular proof theory for various propositional abstract separation logics using cut-free labelled sequent calculi. We first extend the cut-fee labelled sequent calculus for BBI of Hou et al to handle Calcagno et al's original logic of separation algebras by adding sound rules for partial-determinism and cancellativity, while preserving cut-elimination. We prove the completeness of our calculus via a sound intermediate calculus that enables us to construct counter-models from the failure to find a proof. We then capture other propositional abstract separation logics by adding sound rules for indivisible unit and disjointness, while maintaining completeness and cut-elimination. We present a theorem prover based on our labelled calculus for these logics.
Probabilistic coherence spaces are fully abstract for probabilistic PCF
Authors: Ehrhard Thomas , Tasson Christine , Pagani Michele
Published: April 2020

Probabilistic coherence spaces (PCoh) yield a semantics of higher-order probabilistic computation, interpreting types as convex sets and programs as power series. We prove that the equality of interpretations in Pcoh characterizes the operational indistinguishability of programs in PCF with a random primitive.

This is the first result of full abstraction for a semantics of probabilistic PCF. The key ingredient relies on the regularity of power series.

Along the way to the theorem, we design a weighted intersection type assignment system giving a logical presentation of PCoh.
An operational and axiomatic semantics for non-determinism and sequence points in C
Authors: Krebbers Robbert
Published: April 2020

The C11 standard of the C programming language does not specify the execution order of expressions. Besides, to make more effective optimizations possible (eg. delaying of side-effects and interleaving), it gives compilers in certain cases the freedom to use even more behaviors than just those of all execution orders.

Widely used C compilers actually exploit this freedom given by the C standard for optimizations, so it should be taken seriously in formal verification. This paper presents an operational and axiomatic semantics (based on separation logic) for non-determinism and sequence points in C. We prove soundness of our axiomatic semantics with respect to our operational semantics. This proof has been fully formalized using the Coq proof assistant.
A nonstandard standardization theorem
Authors: Accattoli Beniamino , Bonelli Eduardo , Kesner Delia , Lombardi Carlos
Published: April 2020

Standardization is a fundamental notion for connecting programming languages and rewriting calculi. Since both programming languages and calculi rely on substitution for defining their dynamics, explicit substitutions (ES) help further close the gap between theory and practice.

This paper focuses on standardization for the linear substitution calculus, a calculus with ES capable of mimicking reduction in lambda-calculus and linear logic proof-nets. For the latter, proof-nets can be formalized by means of a simple equational theory over the linear substitution calculus.

Contrary to other extant calculi with ES, our system can be equipped with a residual theory in the sense of Lévy, which is used to prove a left-to-right standardization theorem for the calculus with ES but without the equational theory. Such a theorem, however, does not lift from the calculus with ES to proof-nets, because the notion of left-to-right derivation is not preserved by the equational theory. We then relax the notion of left-to-right standard derivation, based on a total order on redexes, to a more liberal notion of standard derivation based on partial orders.

Our proofs rely on Gonthier, Lévy, and Melliès' axiomatic theory for standardization. However, we go beyond merely applying their framework, revisiting some of its key concepts: we obtain uniqueness (modulo) of standard derivations in an abstract way and we provide a coinductive characterization of their key abstract notion of external redex. This last point is then used to give a simple proof that linear head reduction --a nondeterministic strategy having a central role in the theory of linear logic-- is standard.
Improved type specialization for dynamic scripting languages
Authors: Kedlaya Madhukar N. , Roesch Jared , Robatmili Behnam , Reshadi Mehrdad , Hardekopf Ben
Published: April 2020

Type feedback and type inference are two common methods used to optimize dynamic languages such as JavaScript. Each of these methods has its own strengths and weaknesses, and we propose that each can benefit from the other if combined in the right way. We explore the interdependency between these two methods and propose two novel ways to combine them in order to significantly increase their aggregate benefit and decrease their aggregate overhead. In our proposed strategy, an initial type inference pass is applied that can reduce type feedback overhead by enabling more intelligent placement of profiling hooks. This initial type inference pass is novel in the literature. After profiling, a final type inference pass uses the type information from profiling to generate efficient code. While this second pass is not novel, we significantly improve its effectiveness in a novel way by feeding the type inference pass information about the function signature, i.e., the types of the function's arguments for aspecific function invocation. Our results show significant speedups when using these low-overhead strategies, ranging from 1.2x to 4x over an implementation that does not perform type feedback or type inference based optimizations. Our experiments are carried out across a wide range of traditional benchmarks and realistic web applications. The results also show an average reduction of 23.5% in the size of the profiled data for these benchmarks.
Semantics column
Authors: Mislove Michael
Published: April 2020

It's wonderful that SIGLOG is now a reality, thanks to the hard work of so many. It's also an honor to be asked to edit the semantics column for the new SIGLOG Newsletter. In this first column, I want to lay out my goals for the column, and also issue an invitation. The goal is simple: I want this column to be a venue for news of interest to the semantics community, and also to serve as a place where readers from all areas represented within the SIGLOG community can learn about the latest advances in semantics and related areas where semantics plays a role. This includes new research results about the mathematical and logical principles on which semantic models are built, as well as advances in how and where those models are applied. I also hope to include some historical pieces that describe how various advances came about.
Error Control Based Energy Minimization for Cooperative Communication in WSN
Authors: Ahmed Syed Hassan , Kim Dongkyun , Bouk Safdar Hussain , Javaid Nadeem
Published: April 2020

As small-sized nodes are deployed in Wireless Sensor Networks (WSNs), efficient energy utilization becomes a fundamental challenge. Poor channel conditions lead to retransmissions resulting in unnecessary energy usage. To optimize energy consumption and improve network lifetime, error-control strategies are commonly required to manage channel impairments such as noise and fading. Cooperative commu nication is also considered a candidate solution to address the effects of channel fading. Therefore, the energy efficiency of cooperative schemes when applied with Automatic Repeat Request (ARQ), Hybrid-ARQ (HARQ), and Forward Error Correction (FEC) is investigated in this work. Moreover, expressions for energy efficiency of Direct Transmission, Single Relay Cooperation, and Multi Relay Cooperation are derived. Our work focuses on achieving energy-optimal communication in WSNs. Through simulations, it is observed that error-control strategies with a cooperative scheme can significantly enhance system performance in terms of energy optimization.
Automata column
Authors: Bojańczyk Mikołaj
Published: April 2020

In this automata column, Jöel Ouaknine and James Worrell beautifully write about beautiful recent work on linear recurrence sequences, which are sequences of integers defined by recursion like in the Fibonacci sequence. Clearly such sequences can appear almost everywhere, so there is no particularly good reason to talk about them in the automata column, but the authors politely point out such sequences can be used to count the number of words of given length accepted by an automaton. Thanks to this connection we get to have an automata column that cites Terrence Tao and uses logarithms of algebraic numbers.
Algorithmic logic-based verification
Authors: Gurfinkel Arie , Kahsai Temesghen , Navas Jorge A.
Published: April 2020

Turing in his seminal paper "Checking a Large Routine" [Turing 1949] already asked the question whether it was possible to check a routine was
right
. Among other contributions, he proposed flowcharts as a concise program representation. He also described a method based on the insight that a programmer should make a number of definite assertions which can be proven individually, and from which the correctness of the whole program could easily follow. It took several years until Floyd [Floyd 1967] and Hoare [Hoare 1969], inspired by McCarthy [McCarthy 1963] and Naur [Naur 1966]'s works, established a logic based on a deductive system what is called today
Floyd-Hoare logic
that allowed proving correctness of programs in a rigorous manner. Dijkstra [Dijkstra 1975] presented the first semi-algorithmic view of the Floyd-Hoare logic based on the ideas of
predicate transformers
. Since then, the field of software verification has been growing rapidly during the last decades with many available techniques. Among them,
Abstract Interpretation
[Cousot and Cousot 1977],
Model Checking
[Clarke and Emerson 1981; Queille and Sifakis 1982], and
Symbolic Execution
[King 1976] are probably the most predominant algorithmic (i.e., fully automated) techniques today.
Automata and minimization
Authors: Colcombet Thomas , Petrişan Daniela
Published: April 2020

Already in the seventies, strong results illustrating the intimate relationship between category theory and automata theory have been described and are still investigated. In this column, we provide a uniform presentation of the basic concepts that underlie minimization results in automata theory. We then use this knowledge for introducing a new model of automata that is an hybrid of deterministic finite automata and automata weighted over a field. These automata are very natural, and enjoy minimization result by design.

The presentation of this paper is indeed categorical in essence, but it assumes no prior knowledge from the reader. It is also non-conventional in that it is neither algebraic, nor co-algebraic oriented.
Resource semantics
Authors: Pym David
Published: April 2020

The Logic of Bunched Implications (BI) was introduced by O'Hearn and Pym. The original presentation of BI emphasised its role as a system for formal logic (broadly in the tradition of relevant logic) that has some interesting properties, combining a clean proof theory, including a categorical interpretation, with a simple truth-functional semantics. BI quickly found significant applications in program verification and program analysis, chiefly through a specific theory of BI that is commonly known as 'Separation Logic'. We survey the state of work in bunched logics - which, by now, is a quite large family of systems, including modal and epistemic logics and logics for layered graphs - in such a way as to organize the ideas into a coherent (semantic) picture with a strong interpretation in terms of resources. One such picture can be seen as deriving from an interpretation of BI's semantics in terms of
resources,
and this view provides a basis for a systematic interpretation of the family of bunched logics, including modal, epistemic, layered graph, and process-theoretic variants, in terms of resources. We explain the basic ideas of resource semantics, including comparisons with Linear Logic and ideas from economics and physics. We include discussions of BI's λ-calculus, of Separation Logic, and of an approach to distributed systems modelling based on resource semantics.
Conference reports
Authors: Pérez Jorge A
Published: April 2020

In this installment of the conference report column, Michael Morak, Anna Prianichnikova, and Ana Sokolova report on the Helmut Veith MemorialWorkshop 2019, which took place in Turracher Höhe (Austria) during March 17--20, 2019.
Turbo-GTS
Authors: Li Wei , Chen Haiquan , Ku Wei-Shinn , Qin Xiao
Published: April 2020

In mobile crowdsourcing, workers are financially motivated to perform as many self-selected tasks as possible to maximize their revenue. Unfortunately, the existing task scheduling approaches in mobile crowdsourcing fail to consider task execution duration and do not scale for massive tasks and large geographic areas. In this article, we propose a novel framework, Turbo-GTS, in support of large-scale geo-task scheduling, with the objective of identifying an optimal task assignment for each worker to maximize the total number of tasks that can be completed for an entire worker group, given the geographic locations of each task and each worker. Since the exact solution to the geo-task scheduling problem is computationally intractable, we first propose two sub-optimal approaches (least cost neighbor with particle filtering and non-urgency degree particle filtering with iterative clustering) based on particle filtering and DBSCAN for the single-worker geo-task scheduling problem. We then extend our work to solve the multi-worker geo-task scheduling problem by proposing two space partitioning-based methods (QT-NNH and QT-NUD), which leverage point-region quadtree to ensure workload balancing. The effectiveness and efficiency of the four proposed approximate solutions are verified by our extensive experiments using both real and synthetic data. Compared to state-of-the-art approaches, our proposed solutions are able to return a higher number of completed tasks for the worker group while reducing the computation cost by up to three orders of magnitude when coping with massive tasks distributed in large geographic areas.
Dynamic Resource Allocation in Fork-Join Queues
Authors: Marin Andrea , Rossi Sabina , Sottana Matteo
Published: April 2020

Fork-join systems play a pivotal role in the analysis of distributed systems, telecommunication infrastructures, and storage systems. In this article, we consider a fork-join system consisting of
K
parallel servers, each of which works on one of the
K
tasks that form each job. The system allocates a fixed amount of computational resources among the
K
servers, hence determining their service speed. The goal of this article is that of studying the resource allocation policies among the servers. We assume that the queueing disciplines of the fork- and join-queues are First Come First Served. At each epoch, at most
K
tasks are in service while the others wait in the fork-queues. We propose an algorithm with a very simple implementation that allocates the computational resources in a way that aims at minimizing the join-queue lengths, and hence at reducing the expected job service time. We study its performance in saturation and under exponential service time. The model has an elegant closed-form stationary distribution. Moreover, we provide an algorithm to numerically or symbolically derive the marginal probabilities for the join-queue lengths. Therefore, the expressions for the expected join-queue length and the expected response time under immediate join can be derived. Finally, we compare the performance of the proposed resource allocation algorithm with that of other strategies.
Subgame Perfect Equilibria of Sequential Matching Games
Authors: Kawase Yasushi , Yamaguchi Yutaro , Yokoi Yu
Published: April 2020

We study a decentralized matching market in which firms sequentially make offers to potential workers. For each offer, the worker can choose “accept” or “reject,” but the decision is irrevocable. The acceptance of an offer guarantees her job at the firm, but it may also eliminate chances of better offers from other firms in the future. We formulate this market as a perfect-information extensive-form game played by the workers. Each instance of this game has a unique subgame perfect equilibrium (SPE), which does not necessarily lead to a stable matching and has some perplexing properties.

We show a dichotomy result that characterizes the complexity of computing the SPE. The computation is tractable if each firm makes offers to at most two workers or each worker receives offers from at most two firms. In contrast, it is PSPACE-hard even if both firms and workers are related to at most three offers. We also study engineering aspects of this matching market. It is shown that, for any preference profile, we can design an offering schedule of firms so that the worker-optimal stable matching is realized in the SPE.
Adversarial Attacks on Deep-learning Models in Natural Language Processing
Authors: Zhang Wei Emma , Sheng Quan Z. , Alhazmi Ahoud , Li Chenliang
Published: April 2020

With the development of high computational devices, deep neural networks (DNNs), in recent years, have gained significant popularity in many Artificial Intelligence (AI) applications. However, previous efforts have shown that DNNs are vulnerable to strategically modified samples, named
adversarial examples
. These samples are generated with some imperceptible perturbations, but can fool the DNNs to give false predictions. Inspired by the popularity of generating adversarial examples against DNNs in Computer Vision (CV), research efforts on attacking DNNs for Natural Language Processing (NLP) applications have emerged in recent years. However, the intrinsic difference between image (CV) and text (NLP) renders challenges to directly apply attacking methods in CV to NLP. Various methods are proposed addressing this difference and attack a wide range of NLP applications. In this article, we present a systematic survey on these works. We collect all related academic works since the first appearance in 2017. We then select, summarize, discuss, and analyze 40 representative works in a comprehensive way. To make the article self-contained, we cover preliminary knowledge of NLP and discuss related seminal works in computer vision. We conclude our survey with a discussion on open issues to bridge the gap between the existing progress and more robust adversarial attacks on NLP DNNs.