Abstract Stateless model checking (SMC) is crucial for productivity in verified concurrent programming, and its recent developments for C/C++ and weak memory models are remarkable. The state-of-the-art SMC for C, GenMC, efficiently verifies C programs based on C11 atomics and pthreads. However, it does not support mixed-size accesses, accesses to the same memory region with different-sized types, even though they are ubiquitous in C/C++, particularly the code for memory management. As a result, GenMC does not work for C/C++ programs containing memory management. To resolve this problem, we develop a method of adapting GenMC to mixed-size accesses preserving its optimality. We experimentally evaluate the efficiency of our extended implementation of GenMC and its efficacy for memory management programs.

Computational notebook environments are popular and de facto standard tools for programming in data science, whereas computational notebooks are notorious in software engineering. The criticism there stems from the characteristic of facilitating unrestricted dynamic patching of running programs, which makes exploratory coding quick but the resultant code messy and inconsistent. In this work, we first reveal that dynamic patching is a natural demand rather than a mere bad practice in data science programming on Kaggle. We then develop Multiverse Notebook, a computational notebook engine for time-traveling exploration. It enables users to time-travel to any past state and restart with new code from there under state isolation. We present an approach to efficiently implementing time-traveling exploration. We empirically evaluate Multiverse Notebook on ten real-world tasks from Kaggle. Our experiments show that time-traveling exploration on Multiverse Notebook is reasonably efficient.

Non-volatile memory (NVM) is attractive because it enables us to make in-memory data structures persistent without serialization overhead. To implement persistent data structures durable against crashes, periodic checkpointing in NVM has been well studied. A remarkable technique that takes advantage of both DRAM and NVM (i.e., hybrid memory) for periodic checkpointing is mirroring with epoch-based write-address tracking. Its straightforward adoption, however, results in user thread blocking to checkpoint data structures mirrored in DRAM into NVM, from which applications suffer in throughput and responsiveness. To resolve this problem, we incorporate epoch-based versioning into this mirroring technique. The proposed method enables us to delegate checkpointing of data structures mirrored in DRAM into NVM to dedicated background threads that do not block user threads. We develop a system based on our method and evaluate it through experiments with memcached. Our system achieved +13% better throughput than an existing synchronous counterpart and such responsiveness that more than 50% of the performance of the original memcached kept for any time window of 0.5 ms in 99.83% of the entire execution.

Many efforts have recently been made to analyze and validate floating-point errors, particularly in mixed-precision arithmetic. However, real-world applications in approximate computing typically incorporate both model-level approximation and arithmetic-level precision. It is crucial to analyze the combined effects of both precision parameters to the extent valid in terms of approximate algorithms. In this work, we develop a benchmark suite of the practical approximate solvers of various N-body problems that parameterize both N-body approximation and arithmetic precision. It involves precision criteria to prevent us from unrestricted reduced precision and serves as a testbed to analyze the combined effects of model-level approximation and arithmetic-level reduced precision. It would help the design of precision control in approximate computing.

Lexical analysis, which converts input text into a list of tokens, plays an important role in many applications, including compilation and data extraction from texts. To recognize token patterns, a lexer incorporates a sequential computation model - automaton as its basic building component. As such, it is considered difficult to parallelize due to the inherent data dependency. Much work has been done to accelerate lexical analysis through parallel techniques. Unfortunately, existing attempts mainly rely on language-specific remedies for input segmentation, which makes it not only tricky for language extension, but also challenging for automatic lexer generation. This paper presents Plex - an automated tool for generating parallel lexers from user-defined grammars. To overcome the inherent sequentiality, Plex applies a fast prescanning phase to collect context information prior to scanning. To reduce the overheads brought by prescanning, Plex adopts a special automaton, which is derived from that of the scanner, to avoid backtracking behavior and exploits data-parallel techniques. The evaluation under several languages shows that the prescanning overhead is small, and consequently Plex is scalable and achieves 9.8-11.5X speedups using 18 threads.

InfiniBand is a popular high-performance interconnect and offers Remote Direct Memory Access (RDMA), which enables low-latency communication based on kernel bypassing. Although the conventional RDMA technology necessitates manual physical memory management, an emerging extension, On-Demand Paging (ODP), implements automatic memory management based on RDMA-triggered page faults, which benefits productivity. Although the existing studies said the overhead of a page fault of ODP to be small enough, an in-depth investigation in various network situations including retransmission and timeout is missing. In this work, we conduct a comprehensive analysis of the actual behaviors of ODP on different devices and reveal two awful performance pitfalls, which incur longer latencies 3-4 orders of magnitude than a common-case page fault does. We also experimentally demonstrate that the revealed pitfalls are harmful to existing software systems. This paper presents our experimental analysis and lessons learned therefrom.

Parallel reduction, which summarizes a given dataset, e.g., the total, average, and maximum, plays a crucial role in parallel programming. This paper presents a new approach, reverse engineering, to automatically discovering nontrivial parallel reductions in sequential programs. The body of the sequential reduction loop is regarded as a black box, and its input-output behaviors are sampled. If the behaviors correspond to a set of linear polynomials over a semiring, a divide-and-conquer parallel reduction is generated. Auxiliary reverse-engineering methods enable a long and nested loop body to be decomposed, which makes our parallelization scheme applicable to various types of reduction loops. This approach is not only simple and efficient but also agnostic to the details of the input program. Its potential is demonstrated through several use case scenarios. A proof-of-concept implementation successfully inferred linear polynomials for nearly all of the 74 benchmarks exhaustively collected from the literature. These characteristics and experimental results demonstrate the promise of the proposed approach, despite its inherent unsoundness.

Efficient transactional executions are desirable for parallel implementations of algorithms with graph refinements. Hardware transactional memory (HTM) is promising for easy yet efficient transactional executions. Long HTM transactions, however, abort with high probability because of hardware limitations. Unfortunately, Delaunay mesh refinement (DMR), which is an algorithm with graph refinements for mesh generation, causes long transactions. Its parallel implementation naively based on HTM therefore leads to poor performance. To utilize HTM efficiently for parallel implementation of DMR, we present an approach to shortening transactions. Our HTM based implementations of DMR achieved significantly higher throughput and better scalability than a naive HTM-based one and lock-based ones. On a quad-core Has well processor, the absolute speedup of one of our implementations was up to 2.64 with 16 threads.

This paper presents a library called LibDSL that helps the implementer of an embedded domain specific language (EDSL) effectively develop it in D language. The LibDSL library accepts as input some kinds of ``specifications'' of the EDSL that the implementer is going to develop and a D program within which an EDSL source program written by the user is embedded. It produces the front-end code of an LALR parser for the EDSL program and back-end code of the execution engine. LibDSL is able to produce two kinds of execution engines, namely compiler-based and interpreter-based engines, either of which the user can properly choose depending on whether an EDSL program is known at compile time or not. We have implemented the LibDSL system by using template metaprogramming and other advanced facilities such as compile-time function execution of D language. EDSL programs developed by means of LibDSL have a nice integrativeness with the host language.

Existing work that deals with parallelization of complicated reductions and scans focuses only on formalism and hardly dealt with implementation. To bridge the gap between formalism and implementation, we have integrated parallelization via matrix multiplication into compiler construction. Our framework can deal with complicated loops that existing techniques in compilers cannot parallelize. Moreover, we have sophisticated our framework by developing two sets of techniques. One enhances its capability for parallelization by extracting max-operators automatically, and the other improves the performance of parallelized programs by eliminating redundancy. We have also implemented our framework and techniques as a parallelizer in a compiler. Experiments on examples that existing compilers cannot parallelize have demonstrated the scalability of programs parallelized by our implementation.