100 Works

Whole-System WCEC Analysis for Energy-Constrained Real-Time Systems (Artifact)

Peter Wägemann, Christian Dietrich, Tobias Distler, Peter Ulbrich & Wolfgang Schröder-Preikschat
Although internal devices (e.g., memory, timers) and external devices (e.g., sensors, transceivers) significantly contribute to the energy consumption of an embedded real-time system, their impact on the worst-case response energy consumption (WCRE) of tasks is usually not adequately taken into account. Most WCRE analysis techniques only focus on the processor and neglect the energy consumption of other hardware units that are temporarily activated and deactivated in the system. To solve the problem of system-wide energy-consumption...

Contracts in the Wild: A Study of Java Programs (Artifact)

Jens Dietrich, David J. Pearce, Kamil Jezek & Premek Brada
This artefact contains a dataset of open-source programs obtained from the Maven Central Repository and scripts that first extract contracts from these programs and then perform several analyses on the contracts extracted. The extraction and analysis is fully automated and directly produces the tables presented in the accompanying paper. The results show how contracts are used in real-world program, and how their usage changes between versions and within inheritance hierarchies.

DMAC: Deadline-Miss-Aware Control (Artifact)

Paolo Pazzaglia, Claudio Mandrioli, Martina Maggio & Anton Cervin
The real-time implementation of periodic controllers requires solving a co-design problem, in which the choice of the controller sampling period is a crucial element. Classic design techniques limit the period exploration to safe values, that guarantee the correct execution of the controller alongside the remaining real-time load, i.e., ensuring that the controller worst-case response time does not exceed its deadline. This paper presents the artifact linked to DMAC: the first formally-grounded controller design strategy that...

Dependent Types for Class-based Mutable Objects (Artifact)

Joana Campos & Vasco T. Vasconcelos
This artifact is based on DOL, a Dependent Object-oriented Language featuring dependent types, mutable objects and class-based inheritance with subtyping. The typechecker written in Xtend, a flexible and expressive dialect of Java, is a direct implementation of the algorithmic type system described in the companion paper. It uses a direct interface to Z3 theorem prover via its API for Java. The artifact ships with an IDE developed as an Eclipse plugin based on the Xtext...

Scheduling Self-Suspending Tasks: New and Old Results (Artifact)

Jian-Jia Chen, Tobias Hahn, Ruben Hoeksma, Nicole Megow & Georg Von Der Brüggen
In computing systems, a job may suspend itself (before it finishes its execution) when it has to wait for certain results from other (usually external) activities. For real-time systems, such self-suspension behavior has been shown to induce performance degradation. Hence, the researchers in the real-time systems community have devoted themselves to the design and analysis of scheduling algorithms that can alleviate the performance penalty due to self-suspension behavior. As self-suspension and delegation of parts of...

ContextWorkflow: A Monadic DSL for Compensable and Interruptible Executions (Artifact)

Hiroaki Inoue, Tomoyuki Aotani & Atsushi Igarashi
This artifact provides the Scala, Haskell, and Purescript implementations of ContextWorkflow, an embedded domain-specific language for interruptible and compensable executions, and demonstrates the maze search example described in the companion paper. The Haskell and Purescript implementations provide the core language constructs including \texttt{checkpoint} for partial aborts and \texttt{sub} for sub-workflows and show that ContextWorkflow can be embedded in eager and lazy languages as described in the companion paper. The Scala implementation does not only provide...

Object Inheritance Without Classes (Artifact)

Timothy Jones & Michael Homer
This artifact is a PLT Redex implementation of the operational semantics presented in Object Inheritance Without Classes. It defines the core syntax and runtime semantics of the Graceless language, and then extends it in multiple different ways to produce the various implementations of object inheritance, including single and multiple inheritance. The implementation makes the semantics runnable, and precisely defines some behaviour which is defined informally in the paper.

Lightweight Support for Magic Wands in an Automatic Verifier (Artifact)

Malte Schwerhoff & Alexander J. Summers
This artifact is based on Silicon, which is an automatic verification tool for programs written in the Silver Intermediate Verification Language. Silver is designed to natively support permission-based reasoning, in the style of separation logic and similar approaches. Our extension of Silicon provides support for specification and verification of programs using the magic wand operator, which can be used to represent ways to exchange views on the program state, or to represent partial versions of...

Type Abstraction for Relaxed Noninterference (Artifact)

Raimil Cruz, Tamara Rezk, Bernard Serpette & Éric Tanter
This artifact is a web interpreter for the ObSec language defined in the companion paper. ObSec is a simple object-oriented language that supports type-based declassification. Type-base declassification exploits the familiar notion of type abstraction to support expressive declassification policies in a simple and expressive manner.

The Love/Hate Relationship with the C Preprocessor: An Interview Study (Artifact)

Flávio Medeiros, Christian Kästner, Márcio Ribeiro, Sarah Nadi & Rohit Gheyi
This appendix presents detailed information about the research methods we used in the study, subject characterization, grounded theory process that we followed strictly, and the survey we performed in the study. It provides helpful data for understanding the subtler points of the companion paper and for reproducibility.

C++ const and Immutability: An Empirical Study of Writes-Through-const (Artifact)

Jon Eyolfson & Patrick Lam
This artifact is based on ConstSanitizer, a dynamic program analysis tool that detects deep immutability violations through const qualifiers. Our tool instruments any code compiled by clang with the -fsanitizer=const flag. Our implementation includes both instrumentation of LLVM code and a runtime library to support our analysis. The provided package includes our tool and all experiments used in our companion paper. Instructions are also provided.

Brand Objects for Nominal Typing (Artifact)

Timothy Jones, Michael Homer & James Noble
In Brand Objects for Nominal Typing, we describe an implementation of a branding system for both runtime and static types. This artifact provides the extended form of Hopper, an interpreter for the Grace programming language, and extra modules which define both the dynamic objects and the modular static type checker. The extra modules extend the existing structural type checker in the provided version of Hopper, and are capable of statically checking code which interacts with...

TreatJS: Higher-Order Contracts for JavaScript (Artifact)

Matthias Keil & Peter Thiemann
TreatJS is a language embedded, higher-order contract system for JavaScript which enforces contracts by run-time monitoring. Beyond providing the standard abstractions for building higher-order contracts (base, function, and object contracts), TreatJS's novel contributions are its guarantee of non-interfering contract execution, its systematic approach to blame assignment, its support for contracts in the style of union and intersection types, and its notion of a parameterized contract scope, which is the building block for composable run-time generated...

A Theory of Tagged Objects (Artifact)

Joseph Lee, Jonathan Aldrich, Troy Shaw, Alex Potanin & Benjamin Chung
A compiler and interpreter for Wyvern programming language written in Java and hosted on http://github.com/wyvernlang/wyvern and some sample programs (.wyv) including the main example from the paper in borderedwindow.wyv. We also include an extract of all the unit tests of which a large number may be designed to fail -- therefore they are best run using JUnit which can be done by checking out the source tree from the GitHub project link above.

Garbage-Free Abstract Interpretation Through Abstract Reference Counting (Artifact)

Noah Van Es, Quentin Stiévenart & Coen De Roover
This artifact is a modified version of Scala-AM, an abstract interpretation framework implemented in Scala. Specifically, we extended Scala-AM with several implementations of machine abstractions that each employ a different approach to abstract garbage collection. These include traditional (tracing-based) approaches to abstract garbage collection, as well as our own novel approach using abstract reference counting. In particular, using the machine abstraction that employs abstract reference counting (with cycle detection) results in a garbage-free abstract interpreter...

The Eureka Programming Model for Speculative Task Parallelism (Artifact)

Shams Imam & Vivek Sarkar
This artifact includes a Java-based library implementation of the Eureka programming model (EuPM) that simplifies the expression of speculative parallel tasks. Eureka-style computations are especially well-suited for parallel search and optimization applications. The artifact includes implementations of the eureka patterns that are supported by our Eureka API. These patterns include search, optimization, convergence, N-version programming, and soft real-time deadlines. These different patterns of computations can also be safely combined or nested in the EuPM, along...

Fine-grained Language Composition: A Case Study (Artifact)

Edd Barrett, Carl Friedrich Bolz, Lukas Diekmann & Laurence Tratt
This artifact is based on: PyHyp, a language composition of PHP and Python using meta-tracing; and Eco, a language composition editor. The provided package is designed to support the experiments, case studies, and demos detailed in the companion paper.

A Pattern Calculus for Rule Languages: Expressiveness, Compilation, and Mechanization (Artifact)

Avraham Shinnar, Jérôme Siméon & Martin Hirzel
This artifact contains the accompanying code for the ECOOP 2015 paper: "A Pattern Calculus for Rule Languages: Expressiveness, Compilation, and Mechanization". It contains source files for a full mechanization of the three languages presented in the paper: CAMP (Calculus for Aggregating Matching Patterns), NRA (Nested Relational Algebra) and NNRC (Named Nested Relational Calculus). Translations between all three languages and their attendant proofs of correctness are included. Additionally, a mechanization of a type system for the...

A Capability-Based Module System for Authority Control (Artifact)

Darya Melicher, Yangqingwei Shi, Alex Potanin & Jonathan Aldrich
This artifact is intended to demonstrate the module system of the Wyvern programming language and consists of a Linux virtual machine with a snapshot of the Wyvern programming language's codebase. The Wyvern codebase contains a test suite that corresponds to the code examples in the paper accompanying the artifact. In addition, the artifact contains a document describing how to compile and run Wyvern programs.

Evaluations of Push Forward: Global Fixed-Priority Scheduling of Arbitrary-Deadline Sporadic Task Systems (Artifact)

Jian-Jia Chen, Georg Von Der Brüggen & Niklas Ueter
This artifact provides the experimental details and implementations of all the facilitated schedulability tests used in the reported acceptance ratio based evaluations as documented in the related paper "Push Forward: Global Fixed-Priority Scheduling of Arbitrary-Deadline Sporadic Task Systems".

NPM-BUNDLE: Non-Preemptive Multitask Scheduling for Jobs with BUNDLE-Based Thread-Level Scheduling (Artifact)

Corey Tessler & Nathan Fisher
The BUNDLE and BUNDLEP scheduling algorithms are cache-cognizant thread-level scheduling algorithms and associated worst case execution time and cache overhead (WCETO) techniques for hard real-time multi-threaded tasks. The BUNDLE-based approaches utilize the inter-thread cache benefit to reduce WCETO values for jobs. Currently, the BUNDLE-based approaches are limited to scheduling a single task. This work aims to expand the applicability of BUNDLE-based scheduling to multiple task multi-threaded task sets. BUNDLE-based scheduling leverages knowledge of potential cache...

Concurrent Data Structures Linked in Time (Artifact)

Germán Andrés Delbianco, Ilya Sergey, Aleksandar Nanevski & Anindya Banerjee
This artifact provides the full mechanization in FCSL of the developments in the companion paper, "Concurrent Data Structures Linked in Time". In the latter, we propose a new method, based on a separation-style logic, for reasoning about concurrent objects with such linearization points. We embrace the dynamic nature of linearization points, and encode it as part of the data structure's auxiliary state, so that it can be dynamically modified in place by auxiliary code, as...

Dual Priority Scheduling is Not Optimal (Artifact)

Pontus Ekberg
In dual priority scheduling, periodic tasks are executed in a fixed-priority manner, but each job has two phases with different priorities. The second phase is entered after a fixed amount of time has passed since the release of the job, at which point the job changes its priority. Dual priority scheduling was introduced by Burns and Wellings in 1993 and was shown to successfully schedule many task sets that are not schedulable with ordinary (single)...

Type Regression Testing to Detect Breaking Changes in Node.js Libraries (Artifact)

Gianluca Mezzetti, Anders Møller & Martin Toldam Torp
This artifact provides an implementation of a novel technique, type regression testing, to automatically determine whether an update of a npm library implementation affects the types of its public interface, according to how the library is being used by other npm packages. Type regression testing is implemented in the tool NoRegrets. A run of NoRegrets is parameterized with a pre-update and post-update version of the library, and it consists of three fully automatic phases. First,...

LJGS: Gradual Security Types for Object-Oriented Languages (Artifact)

Luminous Fennell & Peter Thiemann
JGS-check is the accompanying artifact to "LJGS: Gradual Security Types for Object-Oriented Languages". LJGS is a Java-like language with gradual security typing. It features a constraint based information flow type system that includes a type dynamic and type casts. Dynamically typed fragments are liberally accepted by the type checker and rely on run-time enforcement for security. JGS-check is a type checker for the subset of Java that corresponds to the calculus presented in the paper...

Registration Year

  • 2015
  • 2016
  • 2017
  • 2018
  • 2019

Resource Types

  • Software