Mark Marron

dblp:88/1390 · DBLP profile ↗
← Back
25ranked-venue papers
13as first author
5since 2021 · last 2026
0000-0003-3589-4860ORCID · corroborated

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

Software engineering, systems software and programming languages · 20 · 11 first-author · 5 since 2021Theory of computation · 2 · 2 first-authorSystems, architecture and hardware · 1Databases, data management, data science and information retrieval · 1Human-computer interaction and ubiquitous computing · 1
YearPublicationVenuePosition
2026 Going Where No GC Has Gone Before: A No-Tradeoff Memory System for Bosque
abstract
Garbage Collectors (GCs) are a critical component of a modern application stack. Long pauses, large memory consumption, and high CPU usage can unexpectedly occur with certain workloads or series of events. These behaviors can make systems unresponsive, make it impossible to run them in resource-constrained environments, and are often very difficult to debug and fix – as their appearance may be intermittent. In fact recent theoretical work has shown what, for existing mainstream languages, these issues are unavoidable and, regardless of the GC design or implementation, there will always be workloads that cause them to occur!
Anthony Arnold, Mark Marron
ISMM2
2024 A Programming Language for Data and Configuration!
abstract
A day in the life of a developer often involves more time working with schemas, configurations, and data description systems than writing code and logic in a classical programming language. As more systems move into distributed worlds, e.g. cloud and microservices, and developers make increasing use of libraries and frameworks, the need to interact with a range of data formats and configuration mechanisms is only increasing. This is a treacherous world, where a misspelled property name or missing field can render an entire service inoperable, a mistake that a number in an API represents seconds instead of milli-seconds can lead to a message being set for delivery in several months instead of in an hour, misconfigured schema can lead to public exposure of sensitive data, and corrupt or erroneous results from a misunderstood data format could result in massive financial and/or reputational damage. To address these challenges this paper casts the problems of data and configuration descriptions, not as a problem of data representation, but as a type system problem, that can be addressed with well understood and highly effective programming language techniques! The novel challenge is that data representation and configuration are universal concerns in a system and, particularly in modern cloud or micro-service systems, these systems may involve many programming languages. In the past this has led to specification systems that use a least-common-denominator set of data types, often little more than strings and numbers, and then rely on conventions or (out-of-date) documentation to ensure that the data is interpreted correctly. This paper shows that, with careful design, it is possible to create a rich universal system that can be used to express data and configuration specifications in a way that is human readable/writable and that can be produced/consumed, much like JSON, by a wide range of programming languages and systems.
Mark Marron
Onward!1
2023 Programming Languages for AI Programing Agents (Invited Talk)
abstract
Over the past decade software development has shifted from a process centered around writing code to a process that increasingly involves composition of external packages and managing the integration of code from other team members. The next decade-plus will be defined by the shift from a process where humans are the central developers of code into one where AI agents, likely Large Language Model (LLM) based, will be the major creators of code and humans will shift to a supervisory role as curators, integrating rich framework-functionality and code developed by AI programming agents.
Mark Marron
DLS1
2023 Toward Programming Languages for Reasoning: Humans, Symbolic Systems, and AI Agents
abstract
Integration, composition, mechanization, and AI assisted development are the driving themes in the future of software development. At their core these concepts are rooted in the increasingly important role of computing in our world, the desire to deliver functionality faster, with higher quality, and to empower more people to benefit from programmatic automation. These themes, and how they impact the human developers driving them, are the foundations for the next generation of programming languages. At first glance the needs of mechanization tools, AI agents, and human developers along with the various goals around development velocity, software quality, and software democratization are a broad and seemingly diverse set of needs. However, at their core is a single challenge that, once resolved, enables us to make radical progress in all of these areas.
Mark Marron
Onward!1
2022 High Assurance Software for Financial Regulation and Business Platforms
Stephen Goldbaum, Attila Mihály, Tosha Ellison, Earl T. Barr, Mark Marron
VMCAI5
2018 Log++ logging for a cloud-native world
abstract
Logging is a fundamental part of the software development and deployment lifecycle but logging support is often provided as an afterthought via limited library APIs or third-party modules. Given the critical nature of logging in modern cloud, mobile, and IoT development workflows, the unique needs of the APIs involved, and the opportunities for optimization using semantic knowledge, we argue logging should be included as a central part of the language and runtime designs. This paper presents a rethinking of the logger for modern cloud-native workflows.
Mark Marron
DLS1
2018 Mining Semantic Loop Idioms
abstract
To write code, developers stitch together patterns, like API protocols or data structure traversals. Discovering these patterns can identify inconsistencies in code or opportunities to replace these patterns with an API or a language construct. We present coiling, a technique for automatically mining code for semantic idioms: surprisingly probable, semantic patterns. We specialize coiling for loop idioms, semantic idioms of loops. First, we show that automatically identifiable patterns exist, in great numbers, with a largescale empirical study of loops over 25MLOC. We find that most loops in this corpus are simple and predictable: 90 percent have fewer than 15LOC and 90 percent have no nesting and very simple control. Encouraged by this result, we then mine loop idioms over a second, buildable corpus. Over this corpus, we show that only 50 loop idioms cover 50 percent of the concrete loops. Our framework opens the door to data-driven tool and language design, discovering opportunities to introduce new API calls and language constructs. Loop idioms show that LINQ would benefit from an Enumerate operator. This can be confirmed by the exitence of a StackOverflow question with 542k views that requests precisely this feature.
Miltiadis Allamanis, Earl T. Barr, Christian Bird, Premkumar T. Devanbu, Mark Marron, Charles Sutton
IEEE Trans. Software Eng.5
2017 Semantics of asynchronous JavaScript
abstract
JavaScript code running in the Node.js runtime is a major platform for developers building cloud, mobile, or IoT applications. A fundamental concept in Node.js programming is the use of asynchronous callbacks and event loops to provide highly responsive applications. While conceptually simple, this programming model contains numerous subtleties and behaviors that are defined implicitly by the current Node.js implementation. This paper presents the first comprehensive formalization of the Node.js asynchronous execution model and defines a high-level notion of async-contexts to formalize fundamental relationships between asynchronous executions in an application. These formalizations provide a foundation for the construction of static or dynamic program analysis tools, support the exploration of alternative Node.js event loop implementations, and provide a high-level conceptual framework for reasoning about relationships between the execution of asynchronous callbacks in a Node.js application.
Matthew C. Loring, Mark Marron, Daan Leijen
DLS2
2016 Program synthesis using natural language
abstract
Interacting with computers is a ubiquitous activity for millions of people. Repetitive or specialized tasks often require creation of small, often one-off, programs. End-users struggle with learning and using the myriad of domain-specific languages (DSLs) to effectively accomplish these tasks.
Aditya Desai, Sumit Gulwani, Vineet Hingorani, Nidhi Jain, Amey Karkare, Mark Marron, Sailesh R, Subhajit Roy 0001
ICSE6
2016 Time-travel debugging for JavaScript/Node.js
abstract
Time-traveling in the execution history of a program during debugging enables a developer to precisely track and understand the sequence of statements and program values leading to an error. To provide this functionality to real world developers, we embarked on a two year journey to create a production quality time-traveling debugger in Microsoft's open-source ChakraCore JavaScript engine and the popular Node.js application framework.
Earl T. Barr, Mark Marron, Ed Maurer, Dan Moseley, Gaurav Seth
SIGSOFT FSE2
2015 User Interaction Models for Disambiguation in Programming by Example
abstract
Programming by Examples (PBE) has the potential to revolutionize end-user programming by enabling end users, most of whom are non-programmers, to create small scripts for automating repetitive tasks. However, examples, though often easy to provide, are an ambiguous specification of the user's intent. Because of that, a key impedance in adoption of PBE systems is the lack of user confidence in the correctness of the program that was synthesized by the system. We present two novel user interaction models that communicate actionable information to the user to help resolve ambiguity in the examples. One of these models allows the user to effectively navigate between the huge set of programs that are consistent with the examples provided by the user. The other model uses active learning to ask directed example-based questions to the user on the test input data over which the user intends to run the synthesized program. Our user studies show that each of these models significantly reduces the number of errors in the performed task without any difference in completion time. Moreover, both models are perceived as useful, and the proactive active-learning based model has a slightly higher preference regarding the users' confidence in the result.
Mikaël Mayer, Gustavo Soares, Maxim Grechkin, Vu Le 0002, Mark Marron, Oleksandr Polozov, Rishabh Singh, Benjamin G. Zorn, Sumit Gulwani
UIST5
2014 Tardis: affordable time-travel debugging in managed runtimes
abstract
Developers who set a breakpoint a few statements too late or who are trying to diagnose a subtle bug from a single core dump often wish for a time-traveling debugger. The ability to rewind time to see the exact sequence of statements and program values leading to an error has great intuitive appeal but, due to large time and space overheads, time traveling debuggers have seen limited adoption. A managed runtime, such as the Java JVM or a JavaScript engine, has already paid much of the cost of providing core features - type safety, memory management, and virtual IO - that can be reused to implement a low overhead time-traveling debugger. We leverage this insight to design and build affordable time-traveling debuggers for managed languages. Tardis realizes our design: it provides affordable time-travel with an average overhead of only 7% during normal execution, a rate of 0.6MB/s of history logging, and a worst-case 0.68s time-travel latency on our benchmark applications. Tardis can also debug optimized code using time-travel to reconstruct state. This capability, coupled with its low overhead, makes Tardis suitable for use as the default debugger for managed languages, promising to bring time-traveling debugging into the mainstream and transform the practice of debugging.
Earl T. Barr, Mark Marron
OOPSLA2
2014 NLyze: interactive programming by natural language for spreadsheet data analysis and manipulation
abstract
Millions of computer end users need to perform tasks over tabular spreadsheet data, yet lack the programming knowledge to do such tasks automatically. This paper describes the design and implementation of a robust natural language based interface to spreadsheet programming. Our methodology involves designing a typed domain-specific language (DSL) that supports an expressive algebra of map, filter, reduce, join, and formatting capabilities at a level of abstraction appropriate for non-expert users. The key algorithmic component of our methodology is a translation algorithm for converting a natural language specification in the context of a given spreadsheet to a ranked set of likely programs in the DSL. The translation algorithm leverages the spreadsheet spatial and temporal context to assign interpretations to specifications with implicit references, and is thus robust to a variety of ways in which end users can express the same task. The translation algorithm builds over ideas from keyword programming and semantic parsing to achieve both high precision and high recall. We implemented the system as an Excel add-in called NLyze that supports a rich user interaction model including annotating the user's natural language specification and explaining the synthesized DSL programs by paraphrasing them into structured English. We collected a total of 3570 English descriptions for 40 spreadsheet tasks and our system was able to generate the intended interpretation as the top candidate for 94% (97 for the top 3) of those instances.
Sumit Gulwani, Mark Marron
SIGMOD Conference2
2013 Collecting a heap of shapes
abstract
The program heap is fundamentally a simple mathematical concept --- a set of objects and a connectivity relation on them. However, a large gap exists between the set of heap structures that could be constructed and those that programmers actually build. To understand this gap, we empirically study heap structures and sharing relations in large object-oriented programs. To scale and make sense of real world heaps, any analysis must employ abstraction; our abstraction groups sets of objects by role and the aliasing present in pointer sets. We find that the heaps of real-world programs are, in practice, fundamentally simple structures that are largely constructed from a small number of simple structures and sharing idioms, such as the sharing of immutable or unique (e.g., singleton) objects. For instance, we find that, under our abstraction, 53--75% of pointers build tree structures and we classify all but 7--18% of aliasing pointers. These results provide actionable information for rethinking the design of annotation systems, memory allocation/collection, and program analyses.
Earl T. Barr, Christian Bird, Mark Marron
ISSTA3
2013 From relational verification to SIMD loop synthesis
abstract
Existing pattern-based compiler technology is unable to effectively exploit the full potential of SIMD architectures. We present a new program synthesis based technique for auto-vectorizing performance critical innermost loops. Our synthesis technique is applicable to a wide range of loops, consistently produces performant SIMD code, and generates correctness proofs for the output code. The synthesis technique, which leverages existing work on relational verification methods, is a novel combination of deductive loop restructuring, synthesis condition generation and a new inductive synthesis algorithm for producing loop-free code fragments. The inductive synthesis algorithm wraps an optimized depth-first exploration of code sequences inside a CEGIS loop. Our technique is able to quickly produce SIMD implementations (up to 9 instructions in 0.12 seconds) for a wide range of fundamental looping structures. The resulting SIMD implementations outperform the original loops by 2.0x-3.7x.
Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, César Kunz, Mark Marron
PPoPP5
2013 Abstracting Runtime Heaps for Program Understanding
abstract
Modern programming environments provide extensive support for inspecting, analyzing, and testing programs based on the algorithmic structure of a program. Unfortunately, support for inspecting and understanding runtime data structures during execution is typically much more limited. This paper provides a general purpose technique for abstracting and summarizing entire runtime heaps. We describe the abstract heap model and the associated algorithms for transforming a concrete heap dump into the corresponding abstract model as well as algorithms for merging, comparing, and computing changes between abstract models. The abstract model is designed to emphasize high-level concepts about heap-based data structures, such as shape and size, as well as relationships between heap structures, such as sharing and connectivity. We demonstrate the utility and computational tractability of the abstract heap model by building a memory profiler. We use this tool to identify, pinpoint, and correct sources of memory bloat for programs from DaCapo.
Mark Marron, César Sánchez 0001, Zhendong Su 0001, Manuel Fähndrich
IEEE Trans. Software Eng.1
2012 Programming Paradigm Driven Heap Analysis
Mark Marron, Ondrej Lhoták, Anindya Banerjee 0001
CC1
2012 Undangle: early detection of dangling pointers in use-after-free and double-free vulnerabilities
abstract
Use-after-free vulnerabilities are rapidly growing in popularity, especially for exploiting web browsers. Use-after-free (and double-free) vulnerabilities are caused by a program operating on a dangling pointer. In this work we propose early detection, a novel runtime approach for finding and diagnosing use-after-free and double-free vulnerabilities. While previous work focuses on the creation of the vulnerability (i.e., the use of a dangling pointer), early detection shifts the focus to the creation of the dangling pointer(s) at the root of the vulnerability. Early detection increases the effectiveness of testing by identifying unsafe dangling pointers in executions where they are created but not used. It also accelerates vulnerability analysis and minimizes the risk of incomplete fixes, by automatically collecting information about all dangling pointers involved in the vulnerability. We implement our early detection technique in a tool called Undangle. We evaluate Undangle for vulnerability analysis on 8 real-world vulnerabilities. The analysis uncovers that two separate vulnerabilities in Firefox had a common root cause and that their patches did not completely fix the underlying bug. We also evaluate Undangle for testing on the Firefox web browser identifying a potential vulnerability.
Juan Caballero, Gustavo Grieco, Mark Marron, Antonio Nappa
ISSTA3
2010 Shape Analysis with Reference Set Relations
Mark Marron, Rupak Majumdar, Darko Stefanovic, Deepak Kapur
VMCAI1
2009 Identification of logically related heap regions
abstract
This paper introduces a novel set of heuristics for identifying logically related sections of the heap such as recursive data structures, objects that are part of the same multi-component structure, and related groups of objects stored in the same collection/array. When combined with lifetime properties of these structures, this information can be used to drive a range of program optimizations including pool allocation, object co-location, static deallocation, and region-based garbage collection. The technique outlined in this paper also improves the efficiency of the static analysis by providing a compact normal form for the abstract models (speeding the convergence of the static analysis).
Mark Marron, Deepak Kapur, Manuel V. Hermenegildo
ISMM1
2008 Efficient Context-Sensitive Shape Analysis with Graph Based Heap Models
Mark Marron, Manuel V. Hermenegildo, Deepak Kapur, Darko Stefanovic
CC1
2008 Sharing analysis of arrays, collections, and recursive structures
abstract
Precise modeling of the program heap is fundamental for understanding the behavior of a program, and is thus of significant interest for many optimization applications. One of the fundamental properties of the heap that can be used in a range of optimization techniques is the sharing relationships between the elements in an array or collection. If an analysis can determine that the memory locations pointed to by different entries of an array (or collection) are disjoint, then in many cases loops that traverse the array can be vectorized or transformed into a thread-parallel version. This paper introduces several novel sharing properties over the concrete heap and corresponding abstractions to represent them. In conjunction with an existing shape analysis technique, these abstractions allow us to precisely resolve the sharing relations in a wide range of heap structures (arrays, collections, recursive data structures, composite heap structures) in a computationally efficient manner. The effectiveness of the approach is evaluated on a set of challenge problems from the JOlden and SPECjvm98 suites. Sharing information obtained from the analysis is used to achieve substantial thread-level parallel speedups.
Mark Marron, Mario Méndez-Lojo, Manuel V. Hermenegildo, Darko Stefanovic, Deepak Kapur
PASTE1
2007 Heap analysis in the presence of collection libraries
abstract
Memory analysis techniques have become sophisticated enough to model, with a high degree of accuracy, the manipulation of simple memory structures (finite structures, single/double linked lists and trees). However, modern programming languages provide extensive library support including a wide range of generic collection objects that make use of complex internal data structures. While these data structures ensure that the collections are efficient, often these representations cannot be effectively modeled by existing methods (either due to excessive analysis runtime or due to the inability to represent the required information). This paper presents a method to represent collections using an abstraction of their semantics. The construction of the abstract semantics for the collection objects is done in a manner that allows individual elements in the collections to be identified. Our construction also supports iterators over the collections and is able to model the position of the iterators with respect to the elements in the collection. By ordering the contents of the collection based on the iterator position, the model can represent a notion of progress when iteratively manipulating the contents of a collection. These features allow strong updates to the individual elements in the collection as well as strong updates over the collections themselves.
Mark Marron, Darko Stefanovic, Manuel V. Hermenegildo, Deepak Kapur
PASTE1
2004 Genomic Distances under Deletions and Insertions
Mark Marron, Krister M. Swenson, Bernard M. E. Moret
Theor. Comput. Sci.1
2003 Genomic Distances under Deletions and Insertions
Mark Marron, Krister M. Swenson, Bernard M. E. Moret
COCOON1