Luís Pina

dblp:98/2164 · DBLP profile ↗
← Back
13ranked-venue papers
5as first author
7since 2021 · last 2026
0000-0003-4585-5259ORCID · corroborated

Domains — the database's venue-derived domains; a paper can count in several

Software engineering, systems software and programming languages · 10 · 3 first-author · 6 since 2021Systems, architecture and hardware · 3 · 3 first-authorArtificial intelligence and machine learning · 1 · 1 since 2021
YearPublicationVenuePosition
2026 Optimizing Record/Replay Through Relaxed Total Ordering and Multi-Version eXecution
abstract
Record/Replay (RR) allows developers to record an execution and then replay it exactly as it was recorded. RR enables deterministic replay of non-deterministic behaviors in a different environment than the one used for the recording, which can capture complex bugs in production and find the root cause during development. Unfortunately, support for RR still introduces a non-negligible amount of performance overhead, which limits its applicability. Two main sources of such overhead in state-of-the-art RR systems are: multi-threading, and I/O bound workloads. To ensure high-fidelity when replaying multi-threading execution, recordings either capture the total order of events, which the replayer then enforces, or capture a partial order that requires further processing before replay. Recording also effectively doubles the I/O performed as the recorder needs to perform the original I/O and then record it to a log. Such increased I/O severely limits the performance of I/O dominated workloads. In this paper, we present two complimentary techniques to reduce the overhead of RR. First, we introduce Relaxed Total Order (RTO), an online-computable weakening of total order that preserves the cross-thread constraints needed for replay while avoiding unnecessary serialization. We design RTO to be compatible with Multi-Version eXecution (MVX), enabling online deterministic replay without pre-processing the recording log or heavyweight coordination. We formalize RTO’s strictness and correctness, showing that it is a novel point between partial- and total-order. Our prototype implementation on top of an existing state-of-the-art RR system reduces recording overhead from 21.0% to 15.3% and halves replay overhead from 67.5% to 31.7%. Second, we combine RR with Multi-Version eXecution (MVX) to eliminate RR’s poor performance on I/O-bound workloads. Our hybrid design uses a follower variant to absorb the extra I/O needed for logging, and to backfill as much I/O as possible from the same underlying system, keeping the user-facing leader off the critical path. Our prototype reduces the overhead required to record I/O bound programs from 192.5% to just 25.5%, without penalizing other more common workloads. Together, RTO and hybrid MVX/RR substantially narrow the gap between today’s RR systems and practical, low-overhead, always-on deployment.
David Schwartz, Luís Pina
ECOOP2
2024 An Empirical Examination of Fuzzer Mutator Performance
abstract
Over the past decade, hundreds of fuzzers have been published in top-tier security and software engineering conferences. Fuzzers are used to automatically test programs, ideally creating high-coverage input corpora and finding bugs. Modern “greybox” fuzzers evolve a corpus of inputs by applying mutations to inputs and then executing those new inputs while collecting coverage. New inputs that are “interesting” (e.g. reveal new coverage) are saved to the corpus. Given their non-deterministic nature, the impact of each design decision on the fuzzer’s performance can be difficult to predict. Some design decisions (e.g., ” Should the fuzzer perform deterministic mutations of inputs? ”) are exposed to end-users as configuration flags, but others (e.g., ” What kinds of random mutations to apply to inputs?”) are typically baked into the fuzzer code itself. This paper describes our over 12.5-CPU-year evaluation of the set of mutation operators employed by the popular AFL++ fuzzer, including the havoc phase, splicing, and, exploring the impact of adjusting some of those unexposed configurations. In this experience paper, we propose a methodology for determining different fuzzers’ behavioral diversity with respect to branch coverage and bug detection using rigorous statistical methods. Our key finding is that, across a range of targets, disabling certain mutation operators (some of which were previously “baked-in” to the fuzzer) resulted in inputs that cover different lines of code and reveal different bugs. A surprising result is disabling certain mutators leads to more diverse coverage and allows the fuzzer to find more bugs faster. We call for researchers to investigate seemingly simple design decisions in fuzzers more thoroughly and encourage fuzzer developers to expose more configuration parameters pertaining to these design decisions to end users.
James Kukucka, Luís Pina, Paul Ammann, Jonathan Bell 0001
ISSTA2
2024 Jmvx: Fast Multi-threaded Multi-version Execution and Record-Replay for Managed Languages
abstract
Multi-version execution (MVX) is a technique that deploys many equivalent versions of the same program — variants — as a single program, with direct application in important fields such as: security, reliability, analysis, and availability. MVX can be seen as “online Record/Replay (RR)”, as RR captures a program’s execution as a log stored on disk that can later be replayed to observe the same execution. Unfortunately, current MVX techniques target programs written in C/C++ and do not support programs written in managed languages, which are the vast majority of code written nowadays. This paper presents the design, implementation, and evaluation of Jmvx— a novel system for performing MVX and RR on programs written in managed languages. Jmvx supports programs written in Java by intercepting automatically identified non-deterministic methods, via a novel dynamic analysis technique, and ensuring that all variants execute the same methods and obtain the same data. Jmvx supports multi-threaded programs, by capturing synchronization operations in one variant, and ensuring all other variants follow the same ordering. We validated that Jmvx supports MVX and RR by applying it to a suite of benchmarks representative of programs written in Java. Internally, Jmvx uses a circular buffer located in shared memory between JVMs to enable fast communication between all variants, averaging 5% |47% performance overhead when performing MVX with multithreading support disabled|enabled, 8% |25% when recording, and 13% |73% when replaying.
David Schwartz, Ankith Kowshik, Luís Pina
Proc. ACM Program. Lang.3
2023 Sinatra: Stateful Instantaneous Updates for Commercial Browsers Through Multi-Version eXecution
abstract
Browsers are the main way in which most users experience the internet, which makes them a prime target for malicious entities. The best defense for the common user is to keep their browser always up-to-date, installing updates as soon as they are available. Unfortunately, updating a browser is disruptive as it results in loss of user state. Even though modern browsers reopen all pages (tabs) after an update to minimize inconvenience, this approach still loses all local user state in each page (e.g., contents of unsubmitted forms, including associated JavaScript validation state) and assumes that pages can be refreshed and result in the same contents. We believe this is an important barrier that keeps users from updating their browsers as frequently as possible. In this paper, we present the design, implementation, and evaluation of Sinatra, which supports instantaneous browser updates that do not result in any data loss through a novel Multi-Version eXecution (MVX) approach for JavaScript programs, combined with a sophisticated proxy. Sinatra works in pure JavaScript, does not require any browser support, thus works on closed-source browsers, and requires trivial changes to each target page, that can be automated. First, Sinatra captures all the non-determinism available to a JavaScript program (e.g., event handlers executed, expired timers, invocations of Math.random). Our evaluation shows that Sinatra requires 6MB to store such events, and the memory grows at a modest rate of 253KB/s as the user keeps interacting with each page. When an update becomes available, Sinatra transfer the state by re-executing the same set of non-deterministic events on the new browser. During this time, which can be as long as 1.5 seconds, Sinatra uses MVX to allow the user to keep interacting with the old browser. Finally, Sinatra changes the roles in less than 10ms, and the user starts interacting with the new browser, effectively performing a browser update with zero downtime and no loss of state.
Ugnius Rumsevicius, Siddhanth Venkateshwaran, Ellen Kidane, Luís Pina
ECOOP4
2022 Reproducibility in Computational Linguistics: Is Source Code Enough?
abstract
The availability of source code has been put forward as one of the most critical factors for improving the reproducibility of scientific research.This work studies trends in source code availability at major computational linguistics conferences; namely, ACL, EMNLP, LREC, NAACL, and COLING.We observe positive trends, especially in conferences that actively promote reproducibility.We follow this by conducting a reproducibility study of eight papers published in EMNLP 2021, finding that source code releases leave much to be desired.Moving forward, we suggest all conferences require self-contained artifacts and provide a venue to evaluate such artifacts at the time of publication.Authors can include small-scale experiments and explicit scripts to generate each result to improve the reproducibility of their work.
Mohammad Arvan, Luís Pina, Natalie Parde
EMNLP2
2022 CONFETTI: Amplifying Concolic Guidance for Fuzzers
abstract
Fuzz testing (fuzzing) allows developers to detect bugs and vulnerabilities in code by automatically generating defect-revealing inputs. Most fuzzers operate by generating inputs for applications and mutating the bytes of those inputs, guiding the fuzzing process with branch coverage feedback via instrumentation. Whitebox guidance (e.g., taint tracking or concolic execution) is sometimes integrated with coverage-guided fuzzing to help cover tricky-to-reach branches that are guarded by complex conditions (so-called "magic values"). This integration typically takes the form of a targeted input mutation, e.g., placing particular byte values at a specific offset of some input in order to cover a branch. However, these dynamic analysis techniques are not perfect in practice, which can result in the loss of important relationships between input bytes and branch predicates, thus reducing the effective power of the technique. We introduce a new, surprisingly simple, but effective technique, global hinting, which allows the fuzzer to insert these interesting bytes not only at a targeted position, but in any position of any input. We implemented this idea in Java, creating Confetti, which uses both targeted and global hints for fuzzing. In an empirical comparison with two baseline approaches, a state-of-the-art greybox Java fuzzer and a version of Confetti without global hinting, we found that Confetti covers more branches and finds 15 previously unreported bugs, including 9 that neither baseline could find. By conducting a post-mortem analysis of Confetti's execution, we determined that global hinting was at least as effective at revealing new coverage as traditional, targeted hinting.
James Kukucka, Luís Pina, Paul Ammann, Jonathan Bell 0001
ICSE2
2022 SaBRe: load-time selective binary rewriting
abstract
Abstract Binary rewriting consists in disassembling a program to modify its instructions. However, existing solutions suffer from shortcomings in terms of soundness and performance. We present SaBRe, a load-time system for selective binary rewriting. SaBRe rewrites specific constructs—particularly system calls and functions—when the program is loaded into memory, and intercepts them using plugins through a simple API. We also discuss the theoretical underpinnings of disassembling and rewriting. We developed two backends—for and —which were used to implement three plugins: a fast system call tracer, a multi-version executor, and a fault injector. Our evaluation shows that SaBRe imposes little overhead, typically below 3%.
Paul-Antoine Arras, Anastasios Andronidis, Luís Pina, Karolis Mituzas, Qianyi Shu, Daniel Grumberg, Cristian Cadar
Int. J. Softw. Tools Technol. Transf.3
2019 MVEDSUA: Higher Availability Dynamic Software Updates via Multi-Version Execution
abstract
Dynamic Software Updating (DSU) is a technique for patching stateful software without shutting it down, which enables both timely updates and non-stop service. Unfortunately, bugs in the update itself---whether in the changed code or in the way the change is introduced dynamically---may cause the updated software to crash or misbehave. Furthermore, the time taken to dynamically apply the update may be unacceptable if it introduces a long delay in service. This paper makes the key observation that both problems can be addressed by employing Multi-Version Execution (MVE). To avoid delay in service, the update is applied to a forked copy while the original system continues to operate. Once the update completes, the MVE system monitors that the responses of both versions agree for the same inputs. Expected divergences are specified by the programmer using an MVE-specific DSL. Unexpected divergences signal possible errors and roll back the update, which simply means terminating the updated version and reverting to the original version. This is safe because the MVE system keeps the state of both versions in sync. If the new version shows no problems after a warmup period, operators can make it permanent and discard the original version. We have implemented this approach, which we call MVEDSUa, by extending the Kitsune DSU framework with Varan, a state-of-the-art MVE system. We have used MVEDSUa to update several high-performance servers: Redis, Memcached, and VSFTPD. Our results show that MVEDSUa significantly reduces the update-time delay, imposes little overhead in steady state, and easily recovers from a
Luís Pina, Anastasios Andronidis, Michael Hicks 0001, Cristian Cadar
ASPLOS1
2018 FreeDA: deploying incompatible stock dynamic analyses in production via multi-version execution
abstract
Dynamic analyses such as those implemented by compiler sanitizers and Valgrind are effective at finding and diagnosing challenging bugs and security vulnerabilities. However, most analyses cannot be combined on the same program execution, and they incur a high overhead, which typically prevents them from being used in production.
Luís Pina, Anastasios Andronidis, Cristian Cadar
CF1
2018 CROCHET: Checkpoint and Rollback via Lightweight Heap Traversal on Stock JVMs
abstract
Checkpoint/rollback (CR) mechanisms create snapshots of the state of a running application, allowing it to later be restored to that checkpointed snapshot. Support for checkpoint/rollback enables many program analyses and software engineering techniques, including test generation, fault tolerance, and speculative execution. Fully automatic CR support is built into some modern operating systems. However, such systems perform checkpoints at the coarse granularity of whole pages of virtual memory, which imposes relatively high overhead to incrementally capture the changing state of a process, and makes it difficult for applications to checkpoint only some logical portions of their state. CR systems implemented at the application level and with a finer granularity typically require complex developer support to identify: (1) where checkpoints can take place, and (2) which program state needs to be copied. A popular compromise is to implement CR support in managed runtime environments, e.g. the Java Virtual Machine (JVM), but this typically requires specialized, non-standard runtime environments, limiting portability and adoption of this approach. In this paper, we present a novel approach for Checkpoint ROllbaCk via lightweight HEap Traversal (Crochet), which enables fully automatic fine-grained lightweight checkpoints within unmodified commodity JVMs (specifically Oracle's HotSpot and OpenJDK). Leveraging key insights about the internal design common to modern JVMs, Crochet works entirely through bytecode rewriting and standard debug APIs, utilizing special proxy objects to perform a lazy heap traversal that starts at the root references and traverses the heap as objects are accessed, copying or restoring state as needed and removing each proxy immediately after it is used. We evaluated Crochet on the DaCapo benchmark suite, finding it to have very low runtime overhead in steady state (ranging from no overhead to 1.29x slowdown), and that it often outperforms a state-of-the-art system-level checkpoint tool when creating large checkpoints.
Jonathan Bell 0001, Luís Pina
ECOOP2
2017 A DSL Approach to Reconcile Equivalent Divergent Program Executions
Luís Pina, Daniel Grumberg, Anastasios Andronidis, Cristian Cadar
USENIX ATC1
2016 Tedsuto: A General Framework for Testing Dynamic Software Updates
abstract
Dynamic software updating (DSU) is a technique for patching running programs, to fix bugs or add new features. DSU avoids the downtime of stop-and-restart updates, but creates new risks -- an incorrect or ill-timed dynamic update could result in a crash or misbehavior, defeating the whole purpose of DSU. To reduce such risks, dynamic updates should be carefully tested before they are deployed. This paper presents Tedsuto, a general testing framework for DSU, along with a concrete implementation of it for Rubah, a state-of-the-art Java-based DSU system. Tedsuto uses system-level tests developed for the old and new versions of the updateable software, and systematically tests whether a dynamic update might result in a test failure. Very often this process is fully automated, while in some cases (e.g., to test new-version functionality) some manual annotations are required. To evaluate Tedsuto's efficacy, we applied it to dynamic updates previously developed (and tested in an ad hoc manner) for the H2 SQL database server and the CrossFTP server -- two real-world, multithreaded systems. We used three large test suites, totalling 446 tests, and we found a variety of update-related bugs quickly, and at low cost.
Luís Pina, Michael Hicks 0001
ICST1
2014 Rubah: DSU for Java on a stock JVM
abstract
This paper presents Rubah, the first dynamic software updating system for Java that: is portable, implemented via libraries and bytecode rewriting on top of a standard JVM; is efficient, imposing essentially no overhead on normal, steady-state execution; is flexible, allowing nearly arbitrary changes to classes between updates; and isnon-disruptive, employing either a novel eager algorithm that transforms the program state with multiple threads, or a novel lazy algorithm that transforms objects as they are demanded, post-update. Requiring little programmer effort, Rubah has been used to dynamically update five long-running applications: the H2 database, the Voldemort key-value store, the Jake2 implementation of the Quake 2 shooter game, the CrossFTP server, and the JavaEmailServer.
Luís Pina, Luís Veiga, Michael Hicks 0001
OOPSLA1