bluuebunny/crossref_metadata_2025 huggingface dataset:
Heterogeneous-race-free memory models
Authors: Hower Derek R. , Hechtman Blake A. , Beckmann Bradford M. , Gaster Benedict R. , Hill Mark D. , Reinhardt Steven K. , Wood David A.
Published: April 2020

Commodity heterogeneous systems (e.g., integrated CPUs and GPUs), now support a unified, shared memory address space for all components. Because the latency of global communication in a heterogeneous system can be prohibi-tively high, heterogeneous systems (unlike homogeneous CPU systems) provide synchronization mechanisms that only guarantee ordering among a subset of threads, which we call a scope. Unfortunately, the consequences and se-mantics of these scoped operations are not yet well under-stood. Without a formal and approachable model to reason about the behavior of these operations, we risk an array of portability and performance issues.

In this paper, we embrace scoped synchronization with a new class of memory consistency models that add scoped synchronization to data-race-free models like those of C++ and Java. Called sequential consistency for heterogeneous-race-free (SC for HRF), the new models guarantee SC for programs with "sufficient" synchronization (no data races) of "sufficient" scope. We discuss two such models. The first, HRF-direct, works well for programs with highly regular parallelism. The second, HRF-indirect, builds on HRF-direct by allowing synchronization using different scopes in some cases involving transitive communication. We quanti-tatively show that HRF-indirect encourages forward-looking programs with irregular parallelism by showing up to a 10% performance increase in a task runtime for GPUs.
Virtual ghost
Authors: Criswell John , Dautenhahn Nathan , Adve Vikram
Published: April 2020

Applications that process sensitive data can be carefully designed and validated to be difficult to attack, but they are usually run on monolithic, commodity operating systems, which may be less secure. An OS compromise gives the attacker complete access to all of an application's data, regardless of how well the application is built. We propose a new system, Virtual Ghost, that protects applications from a compromised or even hostile OS. Virtual Ghost is the first system to do so by combining compiler instrumentation and run-time checks on operating system code, which it uses to create ghost memory that the operating system cannot read or write. Virtual Ghost interposes a thin hardware abstraction layer between the kernel and the hardware that provides a set of operations that the kernel must use to manipulate hardware, and provides a few trusted services for secure applications such as ghost memory management, encryption and signing services, and key management. Unlike previous solutions, Virtual Ghost does not use a higher privilege level than the kernel.

Virtual Ghost performs well compared to previous approaches; it outperforms InkTag on five out of seven of the LMBench microbenchmarks with improvements between 1.3x and 14.3x. For network downloads, Virtual Ghost experiences a 45% reduction in bandwidth at most for small files and nearly no reduction in bandwidth for large files and web traffic. An application we modified to use ghost memory shows a maximum additional overhead of 5% due to the Virtual Ghost protections. We also demonstrate Virtual Ghost's efficacy by showing how it defeats sophisticated rootkit attacks.
Resolved
Authors: Wood David A.
Published: April 2020

The field of computing has struggled since its inception with the tension between specialization and generalization. Specialized architectures, programming languages, and system software promise better performance (across many metrics, including efficiency, productivity, etc.) for workloads that match their specialization objective. General-purpose architectures, languages, and system software sacrifice extremes of performance for specific workloads, seeking acceptable performance across a much wider range. While specialized alternatives have always had their place, general-purpose architectures, languages, and system software have dominated main-stream computing systems for the past several decades. But with Dennard scaling already gone and the end of Moore's Law looming, some have argued that general-purpose computing platforms must naturally give way to specialization.

In this debate, two teams of highly-opinionated experts will debate the proposition that specialized architectures, languages, and system software should largely supplant general-purpose alternatives within the next decade. Arguments in favor of specialization include energy efficiency in the post-Dennard scaling era, performance scaling in the post-Moore's law era, and improvements in programmer productivity. Arguments against include the large investment needed to create specialized hardware and software components, lack of tools and interfaces to create reusable components, the semantic gap from overspecialization, and security vulnerabilities and general correctness issues due to interoperation of specialized components.
The Joint EasyCrypt-F*-CryptoVerif School 2014
Authors: Hriţcu Cătălin
Published: April 2020

Formal security verification tools are slowly reaching maturity. The Joint EasyCrypt-F*-CryptoVerif School took place between 24 and 28 November 2014 in Paris and taught participants how to use three state-of-the-art security verification tools, as well as gave participants a glimpse of the formal foundations behind these tools. The school brought together over 80 participants from 12 countries, with backgrounds spanning security, cryptography, programming languages, and formal methods. The time of the school was roughly evenly split between lectures and hands-on exercise sessions. For the exercise sessions participants installed and tried EasyCrypt, F*, and CryptoVerif on their own laptops, under the guidance of members from the developer teams of the tools. The school also contained three short invited talks: Hubert Comon on
Unconditional Soundness
, Véronique Cortier on
Type-Based Verification of Electronic Voting Protocols
, and Matteo Maffei on
Logical Foundations of Secure Resource Management in Protocol Implementations.
A Practical Getaway
Authors: Stilkerich Isabella , Lang Clemens , Erhardt Christoph , Stilkerich Michael
Published: April 2020

The use of a managed, type-safe language such as Java in real-time and embedded systems offers productivity and, in particular, safety and dependability benefits at a reasonable cost. It has been shown for commodity systems that escape analysis (EA) enables a set of useful optimization, and benefits from the properties of a type-safe language. In this paper, we explore the application of escape analysis in KESO [34], a Java ahead-of-time compiler targeting (deeply) embedded real-time systems. We present specific applications of EA for embedded programs that go beyond the widely known stack-allocation and synchronization optimizations such as extended remote procedure call support for software-isolated applications, automated inference of immutable data or improved upper space and time bounds for worst-case estimations.
Free Rider
Authors: Manilov Stanislav , Franke Björn , Magrath Anthony , Andrieu Cedric
Published: April 2020

Short-vector SIMD and DSP instructions are popular extensions to common Isas. These extensions deliver excellent performance and compact code for some compute-intensive applications, but they require specialised compiler support. To enable the programmer to explicitly request the use of such an instruction, many C compilers provide platform-specific intrinsic functions, whose implementation is handled specially by the compiler. The use of such intrinsics, however, inevitably results in non-portable code. In this paper we develop a novel methodology for retargeting such non-portable code, which maps intrinsics from one platform to another, taking advantage of similar intrinsics on the target platform. We employ a description language to specify the signature and semantics of intrinsics and perform graph-based pattern matching and high-level code transformations to derive optimised implementations exploiting the target's intrinsics, wherever possible. We demonstrate the effectiveness of our new methodology, implemented in the FREE RIDER tool, by automatically retargeting benchmarks derived from OpenCV samples and a complex embedded application optimised to run on an Arm Cortex-M4 to an Intel Edison module with Sse4.2 instructions. We achieve a speedup of up to 3.73 over a plain C baseline, and on average 96.0% of the speedup of manually ported and optimised versions of the benchmarks.
Enabling Efficient Alias Speculation
Authors: Ghosh Soumyadeep , Park Yongjun , Raman Arun
Published: April 2020

Microprocessors designed using HW/SW codesign principles, such as Transmeta™ Efficeon™ and the soon-to-ship NVIDIA 64-bit Tegra® K1, use dynamic binary optimization to extract instruction-level parallelism. Many code optimizations are made significantly more effective through the use of alias speculation. The state-of-the-art alias speculation system, SMARQ, provides 40% speedup on average over a system with no alias speculation. This performance, however, comes at the cost of introducing new alias registers and increased power consumption due to new checks for validating speculation. Consequently, improving the efficiency of alias speculation by reducing alias register requirements and rationalizing speculation validation checks is critical for the viability of SMARQ. This paper presents alias coalescing, a novel technique to significantly improve the efficiency of SMARQ through a synergistic combination of compiler and microarchitectural techniques. By using a more compact encoding for memory access ranges for memory instructions, alias coalescing simultaneously reduces the alias register pressure in SMARQ by a geomean of 26.09% and 39.96%, and the dynamic alias checks by 20.73% and 33.87%, across the entire SPEC CINT2006 and SPEC CFP2006 suites respectively.
StarL
Authors: Lin Yixiao , Mitra Sayan
Published: April 2020

We developed StarL as a framework for programming, simulating, and verifying distributed systems that interacts with physical processes. StarL framework has (a) a collection of distributed primitives for coordination, such as mutual exclusion, registration and geocast that can be used to build sophisticated applications, (b) theory libraries for verifying StarL applications in the PVS theorem prover, and (c) an execution environment that can be used to deploy the applications on hardware or to execute them in a discrete event simulator. The primitives have (i) abstract, nondeterministic specifications in terms of invariants, and assume-guarantee style progress properties, (ii) implementations in Java/Android that always satisfy the invariants and attempt progress using best effort strategies. The PVS theories specify the invariant and progress properties of the primitives, and have to be appropriately instantiated and composed with the application's state machine to prove properties about the application. We have built two execution environments: one for deploying applications on Android/iRobot Create platform and a second one for simulating large instantiations of the applications in a discrete even simulator. The capabilities are illustrated with a StarL application for vehicle to vehicle coordination in an automatic intersection that uses primitives for point-to-point motion, mutual exclusion, and registration.
Implementation-Aware Model Analysis
Authors: Barijough Kamyar Mirzazad , Hashemi Matin , Khibin Volodymyr , Ghiasi Soheil
Published: April 2020

Models of computation abstract away a number of implementation details in favor of well-defined semantics. While this has unquestionable benefits, we argue that analysis of models solely based on operational semantics (implementation-oblivious analysis) is unfit to drive implementation design space exploration. Specifically, we study the tradeoff between buffer size and streaming throughput in applications modeled as synchronous data flow (SDF) graphs. We demonstrate the inherent inaccuracy of implementation-oblivious approach, which only considers SDF operational semantic. We propose a rigorous transformation, which equips the state of the art buffer-throughput tradeoff analysis technique with implementation awareness. Extensive empirical evaluation show that our approach results in significantly more accurate estimates in streaming throughput at the model level, while running two orders of magnitude faster than cycle-accurate simulation of implementations.
Secure and Durable (SEDURA)
Authors: Liu Chen , Yang Chengmo
Published: April 2020

Phase changing memory (PCM) is considered a promising candidate for next-generation main-memory. Despite its advantages of lower power and high density, PCM faces critical security challenges due to its non-volatility: data are still accessible by the attacker even if the device is detached from a power supply. While encryption has been widely adopted as the solution to protect data, it not only creates additional performance and energy overhead during data encryption/decryption, but also hurts PCM lifetime by introducing more writes to PCM cells.

In this paper, we propose a framework that integrates encryption and wear-leveling so as to mitigate the adverse impact of encryption on PCM performance and lifetime. Moreover, by randomizing the address space during wear-leveling, an extra level of protection is provided to the data in memory. We propose two algorithms that respectively prioritize data security and memory lifetime, allowing designers to trade-off between these two factors based on their needs. Compared to previous encryption techniques, the proposed SEDURA framework is able to deliver both more randomness to protect data and more balanced PCM writes, thus effectively balancing the three aspects of data security, application performance, and device lifetime.
TrilobiteG
Authors: Woithe Hans Christian , Kremer Ulrich
Published: April 2020

Programming autonomous systems can be challenging because many programming decisions must be made in real time and under stressful conditions, such as on a battle field, during a short communication window, or during a storm at sea. As such, new programming designs are needed to reflect these specific and extreme challenges.

TrilobiteG is a programming architecture for buoyancy-driven autonomous underwater vehicles (AUVs), called gliders. Gliders are designed to spend weeks to months in the ocean, where they operate fully autonomously while submerged and can only communicate via satellite during their limited time at the surface. Based on the experience gained from a seven year long collaboration with two oceanographic institutes, the TrilobiteG architecture has been developed with the main goal of enabling users to run more effective missions. The TrilobiteG programming environment consists of a domain-specific language called ALGAE, a lower level service layer, and a set of real-time and faster-than-real-time simulators. The system has been used to program novel and robust glider behaviors, as well as to find software problems that otherwise may have remained undetected, with potentially catastrophic results. We believe that TrilobiteG can serve as a blueprint for other autonomous systems as well, and that TrilobiteG will motivate and enable a broader scientific community to work on extreme, real-world problems by using the simulation infrastructure.
Probabilistic bisimulation
Authors: Panangaden Prakash
Published: April 2020

This is a very personal review of the definition of probabilistic bisimulation on continuous state spaces and the logical characterization theorem. I only consider fully probabilistic reactive systems.
You keep using that word
Authors: Cofer Darren
Published: April 2020

Formal methods tools have been shown to be effective at finding defects in and verifying the correctness of safety-critical systems such as avionics systems. The recent release of DO-178C and the accompanying Formal Methods Supplement DO-333 will make it easier for developers of software for commercial aircraft to obtain certification credit for the use of formal methods. However, most developers of avionics systems are unfamiliar with formal methods, and most developers of formal methods tools are unfamiliar with certification requirements and processes. This article provides a brief overview of the certification process for commercial aircraft, as well as some of the issues related to the use of formal methods tools in this context.
Fast and Portable Locking for Multicore Architectures
Authors: Lozi Jean-Pierre , David Florian , Thomas Gaël , Lawall Julia , Muller Gilles
Published: April 2020

The scalability of multithreaded applications on current multicore systems is hampered by the performance of lock algorithms, due to the costs of access contention and cache misses. The main contribution presented in this article is a new locking technique, Remote Core Locking (RCL), that aims to accelerate the execution of critical sections in legacy applications on multicore architectures. The idea of RCL is to replace lock acquisitions by optimized remote procedure calls to a dedicated
server
hardware thread. RCL limits the performance collapse observed with other lock algorithms when many threads try to acquire a lock concurrently and removes the need to transfer lock-protected shared data to the hardware thread acquiring the lock, because such data can typically remain in the server’s cache. Other contributions presented in this article include a profiler that identifies the locks that are the bottlenecks in multithreaded applications and that can thus benefit from RCL, and a reengineering tool that transforms POSIX lock acquisitions into RCL locks.

Eighteen applications were used to evaluate RCL: the nine applications of the SPLASH-2 benchmark suite, the seven applications of the Phoenix 2 benchmark suite, Memcached, and Berkeley DB with a TPC-C client. Eight of these applications are unable to scale because of locks and benefit from RCL on an ×86 machine with four AMD Opteron processors and 48 hardware threads. By using RCL instead of Linux POSIX locks, performance is improved by up to 2.5 times on Memcached, and up to 11.6 times on Berkeley DB with the TPC-C client. On a SPARC machine with two Sun Ultrasparc T2+ processors and 128 hardware threads, three applications benefit from RCL. In particular, performance is improved by up to 1.3 times with respect to Solaris POSIX locks on Memcached, and up to 7.9 times on Berkeley DB with the TPC-C client.
The internet of things… of all things
Authors: Hurlburt George
Published: April 2020

A spendthrift refrigerator, a garrulous cellphone, and a loafing automobile, there's a new technology in town everyone's talking about.
Querying flying robots and other things
Authors: de Leng Daniel
Published: April 2020

A discussion on the role of ontologies and stream reasoning in Internet of Things applications.
Toward computing over encrypted data in IoT systems
Authors: Shafagh Hossein
Published: April 2020

The multitude of IoT devices contributes to the enormous amount of data stored on corporate clouds. Yet the level of computing power has outpaced advances in privacy protection. Could encrypted search preserve the privacy of data, while utilizing the computing power of the cloud?
The ambient intelligence course at Politecnico di Torino
Authors: De Russis Luigi
Published: April 2020

At Italy's oldest technical university, students learn about IoT concepts and technologies by building end-to-end prototypical systems.
Why "celebrate women in computing"?
Authors: Hamdan Nur Al-huda
Published: April 2020

The XRDS blog highlights a range of topics from conference coverage, to security and privacy, to CS theory. Selected blog posts, edited for print, are featured in every issue. Please visit xrds.acm.org/blog to read each post in its entirety. If you are interested in joining as a student blogger, please contact us.
An invitation to game semantics
Authors: Murawski Andrzej S. , Tzevelekos Nikos
Published: April 2020

Game semantics is a flexible semantic theory that has led in recent years to an unprecedented number of full abstraction results for various programming paradigms. We present a gentle introduction to the subject, focussing on high-level ideas and examples with a view to providing a bridge to more technical literature.
Using multi-agent systems to go beyond temporal patterns verification
Authors: Raimondi Franco
Published: April 2020

A key step in formal verification is the translation of
requirements
into
logic formulae
. Various flavours of temporal logic are commonly used in academia and in industry to capture, among others,
liveness
and
safety
requirements. In the past two decades there has been a substantial amount of work in the area of verification of
extensions of temporal logic
. In this column I will provide a high level overview of some work in this area, focussing in particular on the verification of
temporal-epistemic properties
, showing how temporal-epistemic logics can be used to capture requirements that are common in many concrete systems, and describing a model checker for multi-agent systems called MCMAS.
Verification column
Authors: Rungta Neha
Published: April 2020

The technical column on verification presents an invited contribution by César A. Muñoz, Aaron Dutle, Anthony Narkawicz, and Jason Upchurch at NASA Langley Research Center titled
Unmanned Aircraft Systems in the National Airspace System: A Formal Methods Perspective
in the July issue of the SIGLOG newsletter. In the past few years we have seen a dramatic increase in the number of hobbyist unmanned aircraft systems (UAS). In addition we have seen a push by several companies including Amazon to use UAS as a package delivery mechanism. The increasing numbers of UAS in our current airspace have introduced a new safety challenge. There have been some high-profile incidents that were reported widely in the media. One example was a drone being 100 feet within an commercial airliner at the JFK airport in New York in Aug 2015, while another was a near miss at the Los Angeles airport between a Lufthansa passenger jumbo jet and a UAS in March 2016. These are however not isolated incidents. The Federal Aviation Administration (FAA) records shows that there are hundreds of close calls between airplanes and UAS in the US airspace. Similar reports have been documented in the UK and Europe. This safety concern has prompted the development of a detect and avoid capability for the UAS that is designed to avoid aircraft in its vicinity. The article presents the work being done at the NASA Langley Research Center Formal Methods group in Hampton Virigina. I am very excited for this article to appear in the SIGLOG newsletter. This article I believe will be of interest to people not only in the logic, formal methods, and verification community but a broader and more general audience as well.
The 2017 Alonzo Church award
Authors: Panangaden Prakash
Published: April 2020

SIGLOG is delighted to announce that the 2017 Church Award goes to 6 people: Samson Abramsky, Martin Hyland, Radha Jagadeesan, Pasquale Malacaria, Hanno Nickau and Luke Ong for [Quoting from the official citation] "providing a fully-abstract semantics for higher-order computation through the introduction of games models, thereby fundamentally revolutionising the field of programming language semantics, and for the applied impact of these models."
2017 LICS test-of-time award
Authors: Panangaden Prakash
Published: April 2020

To acknowledge the long-term, foundational nature of papers appearing in LICS, the Test-of-Time Award is now awarded every year to the paper or papers that were published in LICS twenty years ago and that have "stood the test of time." The Test-of-Time Award Committee consisting of Christel Baier, Amy Felty (chair), Andrew Pitts and Nicole Schweikardt made two awards in 2017 to honor outstanding papers from the 12th IEEE Symposium on Logic in Computer Science, held 1997 in Warsaw, Poland:
2017 Kleene award
Authors: Panangaden Prakash
Published: April 2020

The LICS conference presents the Kleene Award annually to the best student paper or papers accepted for presentation at LICS that year. This year there were five eligible student papers accepted to LICS 2017. The program committee selected Amina Doumane for the 2017 Kleene Award for her paper "Constructive completeness for the linear-time mu-calculus".
Automata column
Authors: Bojańczyk Mikołaj
Published: April 2020

A central problem of logic in computer science is finding logics for which the satisfiability problem is decidable. A famous non-example is first-order logic, for which satisfiability is undecidable. One method to avoid such undecidability is to find syntactic restrictions on first-order logic (or even stronger logics, like second-order logic), which guarantee that satisfiable formulas have tree-like models, and then to use tree automata to check for the existence of tree-like models. Examples of logics covered by this method include modal logics and guarded logics. In this column, Luc Segoufin surveys the current state of first-order logics with tree-like models, with an emphasis on the newest member of the family, called guarded negation logic.
Complexity column
Authors: Immerman Neil
Published: April 2020

We have learned a great deal about algorithms and computational complexity over the last half century. However, the lack of progress answering certain questions has been stunning. in particular, we have huge trouble proving lower bounds, i.e., that we need at least a certain amount of time or space to solve a particular problem. Here is a beautifully written survey by Ryan Williams explaining some new approaches with which he and his coauthors have achieved state-of-the-art complexity lower bounds. The methods - using the potential power of circuits against themselves - should be particularly appealing to logicians.
Some ways of thinking algorithmically about impossibility
Authors: Williams Ryan
Published: April 2020

Computational complexity lower bounds like P ≠ NP assert impossibility results for all possible programs of some restricted form. As there are presently enormous gaps in our lower bound knowledge, a central question on the minds of today's complexity theorists is
how will we find better ways to reason about all efficient programs?
Systems biology
Authors: Krivine Jean
Published: April 2020

The unequal race between technological and theoretical innovation in Computer Science has a mirror image in Systems Biology where the balance is even more biased toward the experimental side. The aim of Systems Biology is to produce a specification of natural systems, when artificial systems are usually already equipped with one
1
. As a consequence, Systems Biology is almost exclusively an experimental science where most of the innovation effort is geared toward the conception of devices able to extract more facts from biological systems. It has resulted in a modern trend of Systems Biology where high-throughput experiments are now producing big data and a massive inflation of publication volume (Figure 1). The lack of comprehensive integration of biological knowledge is hidden by the success stories of synthetic design using bio material: the initial aim of understanding how the basic components of the cell conspire in a complex and changing environment is modestly replaced by the science of hijacking cellular and genetic components in order to implement intelligently designed tasks. In turn these bio-devices enable biologists to set up more experiments and accumulate more data. This life cycle between technological innovation and data accumulation is encouraged by high impact journals in biology, which tend to give more credit to technological breakthroughs than (disputable) progress in understanding the ways of the cell.
Stochastic process algebras and their markovian semantics
Authors: Hillston Jane
Published: April 2020

There is a long tradition of quantitative modelling in computer and telecommunication systems for performance evaluation and dependability analysis, dating back to the early work of Erlang on telephone exchanges at the beginning of twentieth century [Erlang 1917]. These models are typically stochastic, not because the behaviour of the system under study is inherently random, but because the models usually abstract from data and because interactions with humans are often intrinsic to the system, and both of these give rise to apparently stochastic behaviour. Whilst systems remained of moderate size, models could readily be hand-crafted, and results such as Little's Law were derived and widely-used, for example to optimise job shops [Little 1961]. Much work, like Little's Law, was based on a queueing abstraction, treating the resource in the system as the server of a queue, with users following an appropriate queueing discipline before gaining access to the resource. The more contention there is for the resource, the longer jobs are likely to spend in the queue waiting for access. The queueing paradigm is based on an essentially sequential view of computation and communication, with jobs flowing between resources, completing one task after another. Nevertheless it functioned extremely well until the 1980s, and for many people
performance modelling
was synonymous with
queueing theory.
However, the arrival of distributed systems that allowed jobs to access more than one resource at once, and multicast and broadcast communication, broke the assumptions of basic queueing theory making it much harder to carry out quantitative analysis of stochastic systems in order to predict non-functional properties such as performance, availability, reliability and dependability.
Automata column
Authors: Bojańczyk Mikołaj
Published: April 2020

Last January, the column by Wolfgang Thomas shed new light on the origins of the automata and logic connection, by uncovering the role of Ehrenfeucht in showing that weak monadic second-order logic is decidable over the natural numbers (or over finite words). In this column, Howard Straubing examines another famous part of the automata-logic story, namely the correspondence between aperiodic semigroups and word languages definable in first-order logic. As usual, we discover that the habitual citations are inaccurate, and that the greats knew more than we think.
Complexity column
Authors: Immerman Neil
Published: April 2020

Computer programs are ubiquitous. We depend on them more and more for crucial aspects of our lives. Automatically testing whether programs meet certain safety, security, correctness and fairness conditions is thus crucial. Logic seems to be the most effective tool for meeting this need.
Two-variable logics with counting and semantic constraints
Authors: Kieroński Emanuel , Pratt-Hartmann Ian , Tendera Lidia
Published: April 2020

In this article we discuss fragments and extensions of two-variable logics motivated by practical applications. We outline the decidability frontier, describing some of the techniques developed for deciding satisfiability and finite satisfiability, as well as characterizing their complexity.
Semantics column
Authors: Mislove Michael
Published: April 2020

In this quarter's Semantics column we revisit the topic of Homotopy Type Theory and its applications to constructive mathematics and computation. This continues a theme we began with an overview of the HoTT Program by Steve Awodey and Bob Harper in the January 2015 column [1]. In this month's column, Thierry Coquand describes a number of recent results about
presheaf models of univalence,
which taken together answer some fundamental questions about HoTT. While this is a hot topic among those who have been following its development, it's probably worthwhile reviewing some of the background, for those who aren't familiar with the details. For those who want more information, I recommend Steve and Bob's article, as well as the introduction to the HoTT Book [2].
Conference reports
Authors: Pérez Jorge A
Published: April 2020

This installment of the conference report column includes reports on two recent events related to SIGLOG
Deontic reasoning: from ancient texts to artificial intelligence.
Authors: Ciabattoni Agata , Lellmann Björn , van Berkel Kees
Published: April 2020

The interdisciplinary workshop 'Deontic Reasoning: from Ancient Texts to Artificial Intelligence' (ATAI), bringing together experts from the fields of Logic, Sanskrit, Philosophy, Artificial Intelligence and Law, was held at the Vienna University of Technology (TU Wien) on June 11-13, 2018.
In nuce
, the aim of the workshop was to foster new connections between the aforementioned research areas and facilitate the interchange of ideas with respect to shared grounds of interest, in particular normative reasoning.
Characterizing Output Bottlenecks of a Production Supercomputer
Authors: Xie Bing , Oral Sarp , Zimmer Christopher , Choi Jong Youl , Dillow David , Klasky Scott , Lofstead Jay , Podhorszki Norbert , Chase Jeffrey S.
Published: April 2020

This article studies the I/O write behaviors of the Titan supercomputer and its Lustre parallel file stores under production load. The results can inform the design, deployment, and configuration of file systems along with the design of I/O software in the application, operating system, and adaptive I/O libraries.

We propose a statistical benchmarking methodology to measure write performance across I/O configurations, hardware settings, and system conditions. Moreover, we introduce two relative measures to quantify the write-performance behaviors of hardware components under production load. In addition to designing experiments and benchmarking on Titan, we verify the experimental results on one real application and one real application I/O kernel, XGC and HACC IO, respectively. These two are representative and widely used to address the typical I/O behaviors of applications.

In summary, we find that Titan’s I/O system is variable across the machine at fine time scales. This variability has two major implications. First, stragglers lessen the benefit of coupled I/O parallelism (striping). Peak median output bandwidths are obtained with parallel writes to many independent files, with no striping or write sharing of files across clients (compute nodes). I/O parallelism is most effective when the application—or its I/O libraries—distributes the I/O load so that each target stores files for multiple clients and each client writes files on multiple targets in a balanced way with minimal contention. Second, our results suggest that the potential benefit of dynamic adaptation is limited. In particular, it is not fruitful to attempt to identify “good locations” in the machine or in the file system: component performance is driven by transient load conditions and past performance is not a useful predictor of future performance. For example, we do not observe diurnal load patterns that are predictable.
Efficient Low-Resource Neural Machine Translation with Reread and Feedback Mechanism
Authors: Yu Zhiqiang , Yu Zhengtao , Guo Junjun , Huang Yuxin , Wen Yonghua
Published: April 2020

How to utilize information sufficiently is a key problem in neural machine translation (NMT), which is effectively improved in rich-resource NMT by leveraging large-scale bilingual sentence pairs. However, for low-resource NMT, lack of bilingual sentence pairs results in poor translation performance; therefore, taking full advantage of global information in the encoding-decoding process is effective for low-resource NMT. In this article, we propose a novel reread-feedback NMT architecture (RFNMT) for using global information. Our architecture builds upon the improved sequence-to-sequence neural network and consists of a double-deck attention-based encoder-decoder framework. In our proposed architecture, the information generated by the first-pass encoding and decoding process flows to the second-pass encoding process for more sufficient parameters initialization and information use. Specifically, we first propose a “reread” mechanism to transfer the outputs of the first-pass encoder to the second-pass encoder, and then the output is used for the initialization of the second-pass encoder. Second, we propose a “feedback” mechanism that transfers the first-pass decoder’s outputs to a second-pass encoder via an important weight model and an improved gated recurrent unit (GRU). Experiments on multiple datasets show that our approach achieves significant improvements over state-of-the-art NMT systems, especially in low-resource settings.
S
3
-NET
Authors: Park Cheoneum , Song Heejun , Lee Changki
Published: April 2020

Machine reading comprehension question answering (MRC-QA) is the task of understanding the context of a given passage to find a correct answer within it. A passage is composed of several sentences; therefore, the length of the input sentence becomes longer, leading to diminished performance. In this article, we propose S
3
-NET, which adds sentence-based encoding to solve this problem. S
3
-NET, which is based on a simple recurrent unit architecture, is a deep learning model that solves the MRC-QA by applying matching network to sentence-level encoding. In addition, S
3
-NET utilizes self-matching networks to compute attention weight for its own recurrent neural network sequences. We perform MRC-QA for the SQuAD dataset of English and MindsMRC dataset of Korean. The experimental results show that for SQuAD, the S
3
-NET model proposed in this article produces 71.91% and 74.12% exact match and 81.02% and 82.34% F1 in single and ensemble models, respectively, and for MindsMRC, our model achieves 69.43% and 71.28% exact match and 81.53% and 82.77% F1 in single and ensemble models, respectively.
Uniformly Interpolated Balancing for Robust Prediction in Translation Quality Estimation
Authors: Kim Hyun , Na Seung-Hoon
Published: April 2020

There has been growing interest among researchers in quality estimation (QE), which attempts to automatically predict the quality of machine translation (MT) outputs. Most existing works on QE are based on supervised approaches using quality-annotated training data. However, QE training data quality scores readily become
imbalanced
or
skewed
: QE data are mostly composed of high translation quality sentence pairs but the data lack low translation quality sentence pairs. The use of imbalanced data with an induced quality estimator tends to produce
biased
translation quality scores with “high” translation quality scores assigned even to poorly translated sentences. To address the data imbalance, this article proposes a simple, efficient procedure called
uniformly interpolated balancing
to construct more
balanced
QE training data by inserting greater uniformness to training data. The proposed uniformly interpolated balancing procedure is based on the preparation of two different types of manually annotated QE data: (1)
default skewed data
and (2)
near-uniform data
. First, we obtain default skewed data in a naive manner without considering the imbalance by manually annotating qualities on MT outputs. Second, we obtain near-uniform data in a selective manner by manually annotating a subset only, which is selected from the automatically quality-estimated sentence pairs. Finally, we create
uniformly interpolated balanced data
by combining these two types of data, where one half originates from the default skewed data and the other half originates from the near-uniform data. We expect that uniformly interpolated balancing reflects the intrinsic skewness of the true quality distribution and manages the imbalance problem. Experimental results on an English-Korean quality estimation task show that the proposed uniformly interpolated balancing leads to robustness on both skewed and uniformly distributed quality test sets when compared to the test sets of other non-balanced datasets.
INSTalytics
Authors: Sivathanu Muthian , Vuppalapati Midhul , Gulavani Bhargav S. , Rajan Kaushik , Leeka Jyoti , Mohan Jayashree , Kedia Piyus
Published: April 2020

We present the design, implementation, and evaluation of
INSTalytics
, a co-designed stack of a cluster file system and the compute layer, for efficient big-data analytics in large-scale data centers.
INSTalytics
amplifies the well-known benefits of data partitioning in analytics systems; instead of traditional partitioning on one dimension,
INSTalytics
enables data to be simultaneously partitioned on four different dimensions at the same storage cost, enabling a larger fraction of queries to benefit from partition filtering and joins without network shuffle.

To achieve this,
INSTalytics
uses compute-awareness to customize the three-way replication that the cluster file system employs for availability. A new heterogeneous replication layout enables
INSTalytics
to preserve the same recovery cost and availability as traditional replication.
INSTalytics
also uses compute-awareness to expose a new
sliced-read
API that improves performance of joins by enabling multiple compute nodes to read slices of a data block efficiently via co-ordinated request scheduling and selective caching at the storage nodes.

We have built a prototype implementation of
INSTalytics
in a production analytics stack, and we show that recovery performance and availability is similar to physical replication, while providing significant improvements in query performance, suggesting a new approach to designing cloud-scale big-data analytics systems.
Learning and Modeling Unit Embeddings Using Deep Neural Networks for Unit-Selection-Based Mandarin Speech Synthesis
Authors: Zhou Xiao , Ling Zhen-Hua , Dai Li-Rong
Published: April 2020

A method of learning and modeling unit embeddings using deep neutral networks (DNNs) is presented in this article for unit-selection-based Mandarin speech synthesis. Here, a unit embedding is defined as a fixed-length embedding vector for a phone-sized unit candidate in a corpus. Modeling phone-sized embedding vectors instead of frame-sized acoustic features can better measure the long-term dependencies among consecutive units in an utterance. First, a DNN with an embedding layer is built to learn the embedding vectors of all unit candidates in the corpus from scratch. In order to enable the extracted embedding vectors to carry both acoustic and linguistic information of unit candidates, a multitarget learning strategy is designed for the DNN. Its optional prediction targets include frame-level acoustic features, unit durations, monophone and tone identifiers, and context classes. Then, another two DNNs are constructed to map linguistic features toward the extracted embedding vectors. One of them employs the unit vectors of preceding phones besides the linguistic features of current phone as its input. At synthesis time, the distances between the unit vectors predicted by these two DNNs and the ones derived from unit candidates are used as a part of the target cost and a part of the concatenation cost, respectively. Our experiments on a Mandarin speech synthesis corpus demonstrate that learning and modeling unit embeddings improve the naturalness of hidden Markov model (HMM)-based unit selection speech synthesis. Furthermore, integrating multiple targets for learning unit embeddings achieves better performance than using only acoustic targets according to our subjective evaluation results.
Semantic Role Labeling System for Persian Language
Authors: Mirzaei Azadeh , Sedghi Fatemeh , Safari Pegah
Published: April 2020

In this article, we present an automatic semantic role labeling system in Persian consisting of two modules: argument identification for specifying argument spans and argument classification for categorizing their semantic roles. Our modules have been trained on Persian Proposition Bank in which predicate-argument information is manually added as a layer on top of Persian Dependency Treebank with about 30,000 sentences. Therefore, our system was trained on 216,871 verbal predicates and 42,386 nonverbal ones consisting of 40,813 nouns and 1,573 adjectives with 33 semantic classes. As a supervised method, we used maximum entropy for building an argument identifier that results in human-level accuracy of 99% and support vector machine for an argument classifier with an F1 of 84. Regarding both verbal and nonverbal predicates with an expanded role set, we achieved reasonable results.
The Dilemma of User Engagement in Privacy Notices
Authors: Karegar Farzaneh , Pettersson John Sören , Fischer-Hübner Simone
Published: April 2020

Privacy notices and consent forms are the means of conveying privacy policy information to users. In Europe, a valid consent needs to be confirmed by a clear affirmative action. Despite previous research, it is not yet clear whether user engagement with consent forms via different types of interactions for confirming consent may play a significant role in effectively drawing user attention to the content, even after repeated exposure. We investigate, in a laboratory study, how different types of interactions that engage users with consent forms differ in terms of their effectiveness, efficiency, and user satisfaction. In addition, we examine if and how habituation affects user attention and satisfaction, and the time they spend on giving their consent. We conducted a controlled experiment with 80 participants in four different groups where people either were engaged actively with the policy content via Drag and Drop (DAD), Swipe, or Checkboxes, or were not actively engaged with the content (as the control condition) in a first-exposure phase and in a habituation phase. We measured user attention to consent forms along multiple dimensions, including direct, objective measurements and indirect, self-reported measures. Our results show that the different types of interactions may affect user attention to certain parts of policy information. In particular, the DAD action results in significantly more user attention to the data items compared to other groups. However, with repeated exposure to consent forms, the difference disappears. We conclude that user engagement with policy content needs to be designed with care, so that attention to substantial policy information is increased and not negatively affected.
A Formal Approach to Physics-based Attacks in Cyber-physical Systems
Authors: Lanotte Ruggero , Merro Massimo , Munteanu Andrei , Viganò Luca
Published: April 2020

We apply formal methods to lay and streamline theoretical foundations to reason about Cyber-Physical Systems (CPSs) and physics-based attacks, i.e., attacks targeting physical devices. We focus on a formal treatment of both integrity and denial of service attacks to sensors and actuators of CPSs, and on the timing aspects of these attacks. Our contributions are fourfold. (1) We define a hybrid process calculus to model both CPSs and physics-based attacks. (2) We formalise a threat model that specifies MITM attacks that can manipulate sensor readings or control commands to drive a CPS into an undesired state; we group these attacks into classes and provide the means to assess attack tolerance/vulnerability with respect to a given class of attacks, based on a proper notion of most powerful physics-based attack. (3) We formalise how to estimate the impact of a successful attack on a CPS and investigate possible quantifications of the success chances of an attack. (4) We illustrate our definitions and results by formalising a non-trivial running example in U
PPAAL
SMC, the statistical extension of the U
PPAAL
model checker; we use U
PPAAL
SMC as an automatic tool for carrying out a static security analysis of our running example in isolation and when exposed to three different physics-based attacks with different impacts.