S-REPLS 2018 -- Talks
We Software People are not Worthy - All Hail the Hardware Gods
Sylvan Clebsch
Hardware has advanced leaps and bounds in the last 10 years, but software, and in particular programming languages, are failing to take advantage of this while also holding back the hardware itself. We continue to impose old abstractions on the programming model, such as coherent shared memory, we teach CS students that hash tables have O(1) search, our compilers regularly emit code with suboptimal instruction memory dependence, our memory allocators produce fragmented and unpredictable memory access, and we lean on branch prediction and hardware prefetching to solve our problems. We don’t even use formal verification as much as hardware does. As we move from concurrent computing problems we haven’t solved to distributed computing problems we haven’t imagined, how can we do better? I’ll talk about some of the ways Pony has tried to approach these problems and some of the ways it has failed to do so, I’ll ask why we aren’t all using FORTH, and ask the workshop the big question: are we getting it wrong, or is the hardware not solving the big problems?
Slicing Extended Finite State Machines
Kelly Androutsopoulos
Slicing is a technique, that has traditionally been applied to programs, for extracting the parts of a program that affect the value computed at a statement of interest. It is useful for many Software Engineering applications, including debugging, testing, reuse etc. In recent years, authors have begun to consider slicing at the model level. We consider slicing extended extended finite state machines (EFSMs). They are essentially interactive and may be non-deterministic, so standard techniques for slicing, developed for control flow graphs of programs with a functional semantics, are not immediately applicable. This talk will introduce two algorithms for dependence based slicing of EFSMs, by adapting the commitment closure approach of Danicic et al. We have implemented these algorithms in a tool and conducted experiments on thirteen EFSMs, including benchmark and industrial EFSMs. We report on our findings.
String-diagram Semantics for Functional Languages with Data-flow
Steven Cheung
Geometry of Interaction (GoI) provides a framework for semantics of functional programs in a graphical represen- tation. There have been mainly two styles of GoI, graph rewriting and token passing, recently combined in a com- mon framework.Within this framework we can define abstract machines for modelling higher-order computation under all common reduction strategies. The diagrammatic style allows for the expression of complex semantic rules needed in the formulation of programming languages in which a notion of data flow is essential. In this talk we will show the general idea of GoI semantics and we give specific examples of programming languages for machine learning and incremental computation.This is work in progress jointly with D. R. Ghica and K. Muroya.
Transactions in Relaxed Memory Architectures
Brijesh Dongol
The integration of transactions into hardware relaxed memory architectures is a topic of current research both in industry and academia. In this paper, we provide a general architectural framework for the introduction of transactions into models of relaxed memory in hardware, including the SC, TSO, ARMv8 and PPC models. Our framework incorporates flexible and expressive forms of transaction aborts and execution that have hitherto been in the realm of software transactional memory. In contrast to software transactional memory, we account for the characteristics of relaxed memory as a restricted form of distributed system, without a notion of global time. We prove abstraction theorems to demonstrate that the programmer API matches the intuitions and expectations about transactions.
Fast, Precise Dynamic Checking of Types and Bounds in C
Stephen Kell
Huge amounts of widely-used code are written in C, C++ and other languages which do not enforce any type- or memory-safety invariants. Considerable existing work has added certain kinds of checking, but with caveats: sacrificing source- or binary-level compatibility, imposing high run-time overheads, and mostly ignoring type-correctness. I'll describe libcrunch, a language-agnostic infrastructure for dynamic check in unsafe code (currently C) based on a process-wide model of typed allocations and pluggable disjoint metadata implementations. I'll describe how it permits run-time type checking of pointer casts (not checked by any comparable tool) and, separately, precise bounds checking of pointer and array uses while avoiding various false positives affecting existing "fat pointer" systems.
Safe and Efficient Data Representations for Dynamic Languages with Shared-Memory Parallelism
Stefan Marr
The performance of dynamic languages improved ever since the days of Self. Even so they provide a plethora of features seemingly at odds with an efficient implementation, modern VMs execute programs written in JavaScript, Python, Ruby, or Smalltalk as fast as other less dynamic languages. However, there remains one domain where dynamic languages haven't reached their more conservative counterparts: shared-memory parallelism.
So far, the fewest dynamic language implementations shed their global interpreter locks, which allow for simple and efficient data structures for objects or collections because data races don't have to be considered. The few implementations that did, unfortunately expose applications to data races originating in the VM.
This talk presents work on safe data representations for objects and builtin collections that neither prevent parallel execution nor expose data races originating in VM-level implementation choices. We show that it is possible to avoid any overhead on single threaded code as well as making the data structures scalable for parallel use cases.
Who guards the guards? Formal Validation of the ARM v8-M Architecture Specification
Alastair Reid
Software and hardware are increasingly being formally verified against specifications, but how can we verify the specifications themselves? This talk explores what it means to formally verify a specification. We solve three challenges: (1) How to create a secondary, higher-level speci cation that can be effectively reviewed by processor designers who are not experts in formal verification; (2) How to avoid common-mode failures between the specifications; and (3) How to automatically verify the two specifications against each other.
One of the most important specifications for software verification is the processor specification since it denotes the behaviour of machine code and of hardware protection features used by operating systems. We demonstrate our approach on ARM’s v8-M Processor Specification, which is intended to improve the security of Internet of Things devices. Thus, we focus on establishing the security guarantees the architecture is intended to provide. Despite the fact that the ARM v8-M specification had previously been extensively tested, we found twelve bugs (including two security bugs) that have all been fixed by ARM.
Rule-based Graph Programming
Detlef Plump
This talk introduces GP 2, an experimental rule-based language for solving graph problems. The language is non-deterministic and computationally complete, and has a simple syntax and semantics to facilitate formal reasoning. A number of example programs and their properties will be discussed. Some aspects of our work on GP 2 will be presented, such as program verification with a Hoare-style proof calculus, static confluence checking via critical-pair analysis, and efficient implementation by compilation to C.
