kth.sePublications
Change search
Link to record
Permanent link

Direct link
Publications (10 of 96) Show all publications
Yadav, R., Bauer, M., Broman, D., Garland, M., Aiken, A. & Kjolstad, F. (2025). Automatic Tracing in Task-Based Runtime Systems. In: ASPLOS 2025 - Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems: . Paper presented at 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2025, Rotterdam, Netherlands, Kingdom of the, Mar 30 2025 - Apr 3 2025 (pp. 84-99). Association for Computing Machinery (ACM)
Open this publication in new window or tab >>Automatic Tracing in Task-Based Runtime Systems
Show others...
2025 (English)In: ASPLOS 2025 - Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Association for Computing Machinery (ACM) , 2025, p. 84-99Conference paper, Published paper (Refereed)
Abstract [en]

Implicitly parallel task-based runtime systems often perform dynamic analysis to discover dependencies in and extract parallelism from sequential programs. Dependence analysis becomes expensive as task granularity drops below a threshold. Tracing techniques have been developed where programmers annotate repeated program fragments (traces) issued by the application, and the runtime system memoizes the dependence analysis for those fragments, greatly reducing overhead when the fragments are executed again. However, manual trace annotation can be brittle and not easily applicable to complex programs built through the composition of independent components. We introduce Apophenia, a system that automatically traces the dependence analysis of task-based runtime systems, removing the burden of manual annotations from programmers and enabling new and complex programs to be traced. Apophenia identifies traces dynamically through a series of dynamic string analyses, which find repeated program fragments in the stream of tasks issued to the runtime system. We show that Apophenia is able to come between 0.92x - 1.03x the performance of manually traced programs, and is able to effectively trace previously untraced programs to yield speedups of between 0.91x - 2.82x on the Perlmutter and Eos supercomputers.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2025
Keywords
dynamic analysis, runtime systems, tracing
National Category
Computer Sciences Computer Systems
Identifiers
urn:nbn:se:kth:diva-362694 (URN)10.1145/3669940.3707237 (DOI)2-s2.0-105002385022 (Scopus ID)
Conference
30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2025, Rotterdam, Netherlands, Kingdom of the, Mar 30 2025 - Apr 3 2025
Note

Part of ISBN 9798400706981

QC 20250428

Available from: 2025-04-23 Created: 2025-04-23 Last updated: 2025-04-28Bibliographically approved
Arnstrom, D., Broman, D. & Axehill, D. (2024). Exact Worst-Case Execution-Time Analysis for Implicit Model Predictive Control. IEEE Transactions on Automatic Control, 69(10), 7190-7196
Open this publication in new window or tab >>Exact Worst-Case Execution-Time Analysis for Implicit Model Predictive Control
2024 (English)In: IEEE Transactions on Automatic Control, ISSN 0018-9286, E-ISSN 1558-2523, Vol. 69, no 10, p. 7190-7196Article in journal (Refereed) Published
Abstract [en]

We propose the first method that determines the exact worst-case execution time (WCET) for implicit linear model predictive control (MPC). Such WCET bounds are imperative when MPC is used in real time to control safety-critical systems. The proposed method applies when the quadratic programming solver in the MPC controller belongs to a family of well-established active-set solvers. For such solvers, we leverage a previously proposed complexity certification framework to generate a finite set of "archetypal" optimization problems; we prove that these archetypal problems form an execution-time equivalent cover of all possible problems; that is, that they capture the execution time for solving any possible optimization problem that can be encountered online. Hence, by solving just these archetypal problems on the hardware on which the MPC is to be deployed, and by recording the execution times, we obtain the exact WCET. In addition to providing formal proofs of the methods efficacy, we validate the method on an MPC example where an inverted pendulum on a cart is stabilized. The experiments highlight the following advantages compared with classical WCET methods: first, in contrast to classical static methods, our method gives the exact WCET; second, in contrast to classical measurement-based methods, our method guarantees a correct WCET estimate and requires fewer measurements on the hardware.

Place, publisher, year, edition, pages
Institute of Electrical and Electronics Engineers (IEEE), 2024
Keywords
Execution time analysis, optimization methods, predictive control for linear systems, real time systems
National Category
Control Engineering Computer Systems
Identifiers
urn:nbn:se:kth:diva-354786 (URN)10.1109/TAC.2024.3395521 (DOI)001322635200001 ()2-s2.0-85192183692 (Scopus ID)
Note

QC 20241015

Available from: 2024-10-15 Created: 2024-10-15 Last updated: 2024-10-15Bibliographically approved
Poesia, G., Broman, D., Haber, N. & Goodman, N. D. (2024). Learning Formal Mathematics From Intrinsic Motivation. In: Advances in Neural Information Processing Systems 37 - 38th Conference on Neural Information Processing Systems, NeurIPS 2024: . Paper presented at 38th Conference on Neural Information Processing Systems, NeurIPS 2024, Vancouver, Canada, December 9-15, 2024. Neural information processing systems foundation
Open this publication in new window or tab >>Learning Formal Mathematics From Intrinsic Motivation
2024 (English)In: Advances in Neural Information Processing Systems 37 - 38th Conference on Neural Information Processing Systems, NeurIPS 2024, Neural information processing systems foundation , 2024Conference paper, Published paper (Refereed)
Abstract [en]

How did humanity coax mathematics from the æther? We explore the Platonic view that mathematics can be discovered from its axioms-a game of conjecture and proof. We describe MINIMO (Mathematics from Intrinsic Motivation): an agent that jointly learns to pose challenging problems for itself (conjecturing) and solve them (theorem proving). Given a mathematical domain axiomatized in dependent type theory, we first combine methods for constrained decoding and type-directed synthesis to sample valid conjectures from a language model. Our method guarantees well-formed conjectures by construction, even as we start with a randomly initialized model. We use the same model to represent a policy and value function for guiding proof search. Our agent targets generating hard but provable conjectures-a moving target, since its own theorem proving ability also improves as it trains. We propose novel methods for hindsight relabeling on proof search trees to significantly improve the agent's sample efficiency in both tasks. Experiments on 3 axiomatic domains (propositional logic, arithmetic and group theory) demonstrate that our agent can bootstrap from only the axioms, self-improving in generating true and challenging conjectures and in finding proofs.

Place, publisher, year, edition, pages
Neural information processing systems foundation, 2024
National Category
Other Mathematics
Identifiers
urn:nbn:se:kth:diva-361996 (URN)2-s2.0-105000486976 (Scopus ID)
Conference
38th Conference on Neural Information Processing Systems, NeurIPS 2024, Vancouver, Canada, December 9-15, 2024
Note

Part of ISBN 9798331314385

QC 20250408

Available from: 2025-04-03 Created: 2025-04-03 Last updated: 2025-04-08Bibliographically approved
Opsahl-Ong, K., Ryan, M. J., Purtell, J., Broman, D., Potts, C., Zaharia, M. & Khattab, O. (2024). Optimizing Instructions and Demonstrations for Multi-Stage Language Model Programs. In: EMNLP 2024 - 2024 Conference on Empirical Methods in Natural Language Processing, Proceedings of the Conference: . Paper presented at 2024 Conference on Empirical Methods in Natural Language Processing, EMNLP 2024, Hybrid, Miami, United States of America, November 12-16, 2024 (pp. 9340-9366). Association for Computational Linguistics (ACL)
Open this publication in new window or tab >>Optimizing Instructions and Demonstrations for Multi-Stage Language Model Programs
Show others...
2024 (English)In: EMNLP 2024 - 2024 Conference on Empirical Methods in Natural Language Processing, Proceedings of the Conference, Association for Computational Linguistics (ACL) , 2024, p. 9340-9366Conference paper, Published paper (Refereed)
Abstract [en]

Language Model Programs, i.e. sophisticated pipelines of modular language model (LM) calls, are increasingly advancing NLP tasks. However, building these pipelines requires crafting prompts that are jointly effective for all modules. We study prompt optimization for LM programs, i.e. how to update these prompts to maximize a downstream metric without access to module-level labels or gradients. To make this tractable, we factorize our problem into optimizing the free-form instructions and few-shot demonstrations of every module and introduce several strategies to craft task-grounded instructions and navigate credit assignment across modules. Our strategies include (i) program-and-data-aware techniques for proposing effective instructions, (ii) a stochastic mini-batch evaluation function for learning a surrogate model of our objective, and (iii) a meta-optimization procedure in which we refine how LMs construct proposals over time. Using these insights we develop MIPRO, a novel optimizer that outperforms baselines on five of seven diverse LM programs using a best-in-class open-source model (Llama3-8B), by as much as 13% accuracy. We have released our new optimizers and benchmark in DSPy at http://dspy.ai.

Place, publisher, year, edition, pages
Association for Computational Linguistics (ACL), 2024
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-360569 (URN)10.18653/v1/2024.emnlp-main.525 (DOI)2-s2.0-85217816148 (Scopus ID)
Conference
2024 Conference on Empirical Methods in Natural Language Processing, EMNLP 2024, Hybrid, Miami, United States of America, November 12-16, 2024
Note

Part of ISBN 9798891761643

QC 20250227

Available from: 2025-02-26 Created: 2025-02-26 Last updated: 2025-02-27Bibliographically approved
Çaylak, G., Lundén, D., Senderov, V. & Broman, D. (2024). Statically and Dynamically Delayed Sampling for Typed Probabilistic Programming Languages. In: Laemmel, R Pereira, JA Mosses, PD (Ed.), PROCEEDINGS OF THE 17TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON SOFTWARE LANGUAGE ENGINEERING, SLE 2024: . Paper presented at 17th ACM SIGPLAN International Conference on Software Language Engineering (SLE), OCT 20-21, 2024, Pasadena, CA (pp. 157-170). Association for Computing Machinery (ACM)
Open this publication in new window or tab >>Statically and Dynamically Delayed Sampling for Typed Probabilistic Programming Languages
2024 (English)In: PROCEEDINGS OF THE 17TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON SOFTWARE LANGUAGE ENGINEERING, SLE 2024 / [ed] Laemmel, R Pereira, JA Mosses, PD, Association for Computing Machinery (ACM) , 2024, p. 157-170Conference paper, Published paper (Refereed)
Abstract [en]

Probabilistic programming languages (PPLs) make it possible to separate the concerns between probabilistic models and Bayesian inference algorithms. However, to make such inference efficient is technically very challenging, both in terms of execution time performance and inference accuracy. One successful optimization approach is the previously published work on dynamically delayed sampling. This runtime method makes use of analytical relations between random variables to reduce inference variance; however, tracking these relations introduces runtime overhead. Furthermore, implementing the dynamic approach in a statically typed language introduces type problems because delaying the sampling of random variables changes their types. Our work advances the state-of-the-art in two aspects. Firstly, to reduce the runtime overhead, we develop a compile-time version of delayed sampling. By incorporating optimization procedures during compilation, we eliminate the need for runtime relation tracking and consequent overhead. However, the compile-time version may not always be effective due to the program's possible dynamic behavior, such as stochastic branches, or the complexity of handling recursion. Secondly, we introduce constructs to implement dynamically delayed sampling in a statically typed universal PPL. Dynamically delayed sampling in statically typed languages is a viable optimization for complex Bayesian models, whereas simple models ought to be statically optimized. We evaluate both statically and dynamically delayed sampling on real-world examples, such as latent Dirichlet allocation and epidemiology models, and implement the methods in a statically typed PPL, Miking CorePPL.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2024
Keywords
Probabilistic Programming, Bayesian Inference, Delayed Sampling, Automation
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-357520 (URN)10.1145/3687997.3695634 (DOI)001344239100013 ()2-s2.0-85210864623 (Scopus ID)
Conference
17th ACM SIGPLAN International Conference on Software Language Engineering (SLE), OCT 20-21, 2024, Pasadena, CA
Note

Part of ISBN 979-8-4007-1180-0

QC 20241209

Available from: 2024-12-09 Created: 2024-12-09 Last updated: 2025-05-27Bibliographically approved
Lundén, D., Hummelgren, L., Kudlicka, J., Eriksson, O. & Broman, D. (2024). Suspension Analysis and Selective Continuation-Passing Style for Universal Probabilistic Programming Languages. In: Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings: . Paper presented at 33rd European Symposium on Programming, ESOP 2024, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, Apr 6 2024 - Apr 11 2024 (pp. 302-330). Springer Nature, 14577
Open this publication in new window or tab >>Suspension Analysis and Selective Continuation-Passing Style for Universal Probabilistic Programming Languages
Show others...
2024 (English)In: Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Proceedings, Springer Nature , 2024, Vol. 14577, p. 302-330Conference paper, Published paper (Refereed)
Abstract [en]

Universal probabilistic programming languages (PPLs) make it relatively easy to encode and automatically solve statistical inference problems. To solve inference problems, PPL implementations often apply Monte Carlo inference algorithms that rely on execution suspension. State-of-the-art solutions enable execution suspension either through (i) continuation-passing style (CPS) transformations or (ii) efficient, but comparatively complex, low-level solutions that are often not available in high-level languages. CPS transformations introduce overhead due to unnecessary closure allocations—a problem the PPL community has generally overlooked. To reduce overhead, we develop a new efficient selective CPS approach for PPLs. Specifically, we design a novel static suspension analysis technique that determines parts of programs that require suspension, given a particular inference algorithm. The analysis allows selectively CPS transforming the program only where necessary. We formally prove the correctness of the analysis and implement the analysis and transformation in the Miking CorePPL compiler. We evaluate the implementation for a large number of Monte Carlo inference algorithms on real-world models from phylogenetics, epidemiology, and topic modeling. The evaluation results demonstrate significant improvements across all models and inference algorithms.

Place, publisher, year, edition, pages
Springer Nature, 2024
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 14577
Keywords
Continuation-passing style, Probabilistic programming, Static analysis
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-346543 (URN)10.1007/978-3-031-57267-8_12 (DOI)001281762600012 ()2-s2.0-85192176283 (Scopus ID)
Conference
33rd European Symposium on Programming, ESOP 2024, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, Apr 6 2024 - Apr 11 2024
Note

QC 20240521

Part of ISBN 978-303157266-1

Available from: 2024-05-16 Created: 2024-05-16 Last updated: 2024-09-12Bibliographically approved
Hummelgren, L., Palmkvist, V., Stjerna, L., Xu, X., Jaldén, J. & Broman, D. (2024). Trellis: A Domain-Specific Language for Hidden Markov Models with Sparse Transitions. In: Laemmel, R Pereira, JA Mosses, PD (Ed.), PROCEEDINGS OF THE 17TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON SOFTWARE LANGUAGE ENGINEERING, SLE 2024: . Paper presented at 17th ACM SIGPLAN International Conference on Software Language Engineering (SLE), OCT 20-21, 2024, Pasadena, CA (pp. 196-209). Association for Computing Machinery (ACM)
Open this publication in new window or tab >>Trellis: A Domain-Specific Language for Hidden Markov Models with Sparse Transitions
Show others...
2024 (English)In: PROCEEDINGS OF THE 17TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON SOFTWARE LANGUAGE ENGINEERING, SLE 2024 / [ed] Laemmel, R Pereira, JA Mosses, PD, Association for Computing Machinery (ACM) , 2024, p. 196-209Conference paper, Published paper (Refereed)
Abstract [en]

Hidden Markov models (HMMs) are frequently used in areas such as speech recognition and bioinformatics. However, implementing HMM algorithms correctly and efficiently is time-consuming and error-prone. Specifically, using model-specific knowledge to improve performance, such as sparsity in the transition probability matrix, ties the implementation to a particular model, making it harder to modify. Previous work has introduced high-level frameworks for defining HMMs, thus lifting the burden of efficiently implementing HMM algorithms from the user. However, existing tools are ill-suited for sparse HMMs with many states. This paper introduces Trellis, a domain-specific language for succinctly defining sparse HMMs that use GPU acceleration to achieve high performance. We show that Trellis outperforms previous work and is on par with a hand-written CUDA kernel implementation for a particular sparse HMM.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2024
Keywords
HiddenMarkovmodels, DSL, parallelization, GPU acceleration
National Category
Probability Theory and Statistics
Identifiers
urn:nbn:se:kth:diva-357515 (URN)10.1145/3687997.3695641 (DOI)001344239100017 ()2-s2.0-85210805499 (Scopus ID)
Conference
17th ACM SIGPLAN International Conference on Software Language Engineering (SLE), OCT 20-21, 2024, Pasadena, CA
Note

Part of ISBN 979-8-4007-1180-0

QC 20241209

Available from: 2024-12-09 Created: 2024-12-09 Last updated: 2025-05-27Bibliographically approved
Lundén, D., Çaylak, G., Ronquist, F. & Broman, D. (2023). Automatic Alignment in Higher-Order Probabilistic Programming Languages. In: Programming Languages and Systems: . Paper presented at 32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023.. Springer Nature
Open this publication in new window or tab >>Automatic Alignment in Higher-Order Probabilistic Programming Languages
2023 (English)In: Programming Languages and Systems, Springer Nature , 2023Conference paper, Published paper (Refereed)
Abstract [en]

Probabilistic Programming Languages (PPLs) allow users to encode statistical inference problems and automatically apply an inference algorithm to solve them. Popular inference algorithms for PPLs, such as sequential Monte Carlo (SMC) and Markov chain Monte Carlo (MCMC), are built around checkpoints—relevant events for the inference algorithm during the execution of a probabilistic program. Deciding the location of checkpoints is, in current PPLs, not done optimally. To solve this problem, we present a static analysis technique that automatically determines checkpoints in programs, relieving PPL users of this task. The analysis identifies a set of checkpoints that execute in the same order in every program run—they are aligned. We formalize alignment, prove the correctness of the analysis, and implement the analysis as part of the higher-order functional PPL Miking CorePPL. By utilizing the alignment analysis, we design two novel inference algorithm variants: aligned SMC and aligned lightweight MCMC. We show, through real-world experiments, that they significantly improve inference execution time and accuracy compared to standard PPL versions of SMC and MCMC.

Place, publisher, year, edition, pages
Springer Nature, 2023
Series
Lecture Notes in Computer Science ; 13990
Keywords
Probabilistic programming, Operational semantics, Static analysis
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:kth:diva-324293 (URN)10.1007/978-3-031-30044-8_20 (DOI)001284040300020 ()2-s2.0-85161447105 (Scopus ID)
Conference
32nd European Symposium on Programming, ESOP 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22–27, 2023.
Note

QC 20230227

Available from: 2023-02-24 Created: 2023-02-24 Last updated: 2024-09-27
Lohstroh, M., Lee, E. A., Edwards, S. A. & Broman, D. (2023). Logical Time for Reactive Software. In: Proceedings of 2023 Cyber-Physical Systems and Internet-of-Things Week, CPS-IoT Week 2023: Workshops. Paper presented at 2023 Cyber-Physical Systems and Internet-of-Things Week, CPS-IoT Week 2023, San Antonio, United States of America, May 9 2023 - May 12 2023 (pp. 313-318). Association for Computing Machinery (ACM)
Open this publication in new window or tab >>Logical Time for Reactive Software
2023 (English)In: Proceedings of 2023 Cyber-Physical Systems and Internet-of-Things Week, CPS-IoT Week 2023: Workshops, Association for Computing Machinery (ACM) , 2023, p. 313-318Conference paper, Published paper (Refereed)
Abstract [en]

Timing is an essential feature of reactive software. It is not just a performance metric, but rather forms a core part of the semantics of programs. This paper argues for a notion of logical time that serves as an engineering model to complement a notion of physical time, which models the physical passage of time. Programming models that embrace logical time can provide deterministic concurrency, better analyzability, and practical realizations of timing-sensitive applications. We give definitions for physical and logical time and review some languages and formalisms that embrace logical time.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2023
Keywords
programming model, reactive systems, software, timing
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-333297 (URN)10.1145/3576914.3587494 (DOI)001054880600055 ()2-s2.0-85159781950 (Scopus ID)
Conference
2023 Cyber-Physical Systems and Internet-of-Things Week, CPS-IoT Week 2023, San Antonio, United States of America, May 9 2023 - May 12 2023
Note

Part of ISBN 9798400700491

QC 20230801

Available from: 2023-08-01 Created: 2023-08-01 Last updated: 2023-10-16Bibliographically approved
Truszkowski, J., Perrigo, A., Broman, D., Ronquist, F. & Antonelli, A. (2023). Online tree expansion could help solve the problem of scalability in Bayesian phylogenetics. Systematic Biology, Article ID syad045.
Open this publication in new window or tab >>Online tree expansion could help solve the problem of scalability in Bayesian phylogenetics
Show others...
2023 (English)In: Systematic Biology, ISSN 1063-5157, E-ISSN 1076-836X, article id syad045Article in journal (Refereed) Published
Abstract [en]

Bayesian phylogenetics is now facing a critical point. Over the last 20 years, Bayesian methods have reshaped phylogenetic inference and gained widespread popularity due to their high accuracy, the ability to quantify the uncertainty of inferences and the possibility of accommodating multiple aspects of evolutionary processes in the models that are used. Unfortunately, Bayesian methods are computationally expensive, and typical applications involve at most a few hundred sequences. This is problematic in the age of rapidly expanding genomic data and increasing scope of evolutionary analyses, forcing researchers to resort to less accurate but faster methods, such as maximum parsimony and maximum likelihood. Does this spell doom for Bayesian methods? Not necessarily. Here, we discuss some recently proposed approaches that could help scale up Bayesian analyses of evolutionary problems considerably. We focus on two particular aspects: online phylogenetics, where new data sequences are added to existing analyses, and alternatives to Markov chain Monte Carlo (MCMC) for scalable Bayesian inference. We identify 5 specific challenges and discuss how they might be overcome. We believe that online phylogenetic approaches and Sequential Monte Carlo hold great promise and could potentially speed up tree inference by orders of magnitude. We call for collaborative efforts to speed up the development of methods for real-time tree expansion through online phylogenetics.

Place, publisher, year, edition, pages
Oxford University Press (OUP), 2023
Keywords
Bayesian inference, MCMC, phylogeny, sequential Monte Carlo
National Category
Bioinformatics and Computational Biology
Identifiers
urn:nbn:se:kth:diva-336995 (URN)10.1093/sysbio/syad045 (DOI)001058101900001 ()37498209 (PubMedID)2-s2.0-85177488121 (Scopus ID)
Note

QC 20230922

Available from: 2023-09-22 Created: 2023-09-22 Last updated: 2025-02-07Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0001-8457-4105

Search in DiVA

Show all publications