uu.seUppsala University Publications
Change search
Link to record
Permanent link

Direct link
BETA
Jonsson, Bengt
Alternative names
Publications (10 of 100) Show all publications
Lindén, J., Bauer, P., Engblom, S. & Jonsson, B. (2019). Exposing inter-process information for efficient PDES of spatial stochastic systems on multicores. ACM Transactions on Modeling and Computer Simulation, 29(2), 11:1-25, Article ID 11.
Open this publication in new window or tab >>Exposing inter-process information for efficient PDES of spatial stochastic systems on multicores
2019 (English)In: ACM Transactions on Modeling and Computer Simulation, ISSN 1049-3301, E-ISSN 1558-1195, Vol. 29, no 2, p. 11:1-25, article id 11Article in journal (Refereed) Published
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-342180 (URN)10.1145/3301500 (DOI)000468031300004 ()
Projects
UPMARC
Available from: 2019-04-02 Created: 2018-02-19 Last updated: 2019-06-18Bibliographically approved
Lindén, J. & Jonsson, B. (2018). A Skiplist-Based Concurrent Priority Queue with Minimal Memory Contention.
Open this publication in new window or tab >>A Skiplist-Based Concurrent Priority Queue with Minimal Memory Contention
2018 (English)Report (Other academic)
Series
Technical report / Department of Information Technology, Uppsala University, ISSN 1404-3203 ; 2018-003
Keywords
Concurrent Data Structures, Priority Queue, Lock-free, Non-blocking, Skiplist
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-342233 (URN)
Projects
CoDeR-MPUPMARC
Available from: 2018-02-19 Created: 2018-02-19 Last updated: 2018-04-06Bibliographically approved
Cassel, S., Howar, F., Jonsson, B. & Steffen, B. (2018). Extending Automata Learning to Extended Finite State Machines. In: Bennaceur, A Hahnle, R Meinke, K (Ed.), Machine Learning for Dynamic Software Analysis: Potentials and Limits. Paper presented at International Dagstuhl Seminar on 16172 - Machine Learning for Dynamic Software Analysis - Potentials and Limits, APR 24-27, 2016, Wadern, GERMANY (pp. 149-177). Springer
Open this publication in new window or tab >>Extending Automata Learning to Extended Finite State Machines
2018 (English)In: Machine Learning for Dynamic Software Analysis: Potentials and Limits / [ed] Bennaceur, A Hahnle, R Meinke, K, Springer, 2018, p. 149-177Conference paper, Published paper (Refereed)
Abstract [en]

Automata learning is an established class of techniques for inferring automata models by observing how they respond to a sample of input words. Recently, approaches have been presented that extend these techniques to infer extended finite state machines (EFSMs) by dynamic black-box analysis. EFSMs model both data flow and control behavior, and their mutual interaction. Different dialects of EFSMs are widely used in tools for model-based software development, verification, and testing. This survey paper presents general principles behind some of these recent extensions. The goal is to elucidate how the principles behind classic automata learning can be maintained and guide extensions to more general automata models, and to situate some extensions with respect to these principles.

Place, publisher, year, edition, pages
Springer, 2018
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 11026
National Category
Control Engineering
Identifiers
urn:nbn:se:uu:diva-391442 (URN)10.1007/978-3-319-96562-8_6 (DOI)000476941200006 ()978-3-319-96562-8 (ISBN)978-3-319-96561-1 (ISBN)
Conference
International Dagstuhl Seminar on 16172 - Machine Learning for Dynamic Software Analysis - Potentials and Limits, APR 24-27, 2016, Wadern, GERMANY
Funder
EU, FP7, Seventh Framework Programme, IST 231167Swedish Research Council
Available from: 2019-08-22 Created: 2019-08-22 Last updated: 2019-08-22Bibliographically approved
Lindén, J., Bauer, P., Engblom, S. & Jonsson, B. (2018). Fine-grained local dynamic load balancing in PDES. In: Proc. 6th ACM SIGSIM Conference on Principles of Advanced Discrete Simulation: . Paper presented at SIGSIM-PADS 2018 (pp. 201-212). New York: ACM Press
Open this publication in new window or tab >>Fine-grained local dynamic load balancing in PDES
2018 (English)In: Proc. 6th ACM SIGSIM Conference on Principles of Advanced Discrete Simulation, New York: ACM Press, 2018, p. 201-212Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
New York: ACM Press, 2018
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-342174 (URN)10.1145/3200921.3200928 (DOI)000482913900025 ()978-1-4503-5092-1 (ISBN)
Conference
SIGSIM-PADS 2018
Projects
UPMARC
Available from: 2018-05-14 Created: 2018-02-19 Last updated: 2019-10-21Bibliographically approved
Abdulla, P. A., Jonsson, B. & Trinh, C. Q. (2018). Fragment abstraction for concurrent shape analysis. In: Programming Languages and Systems: . Paper presented at ESOP 2018 (pp. 442-471). Springer
Open this publication in new window or tab >>Fragment abstraction for concurrent shape analysis
2018 (English)In: Programming Languages and Systems, Springer, 2018, p. 442-471Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer, 2018
Series
Lecture Notes in Computer Science ; 10801
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-368505 (URN)10.1007/978-3-319-89884-1_16 (DOI)978-3-319-89883-4 (ISBN)
Conference
ESOP 2018
Projects
UPMARC
Available from: 2018-04-14 Created: 2018-12-05 Last updated: 2018-12-07Bibliographically approved
Winblad, K., Sagonas, K. & Jonsson, B. (2018). Lock-free Contention Adapting Search Trees. In: The 30th ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2018: . Paper presented at The 30th ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2018, July 16–18, 2018, Vienna, Austria. New York, NY, USA, 30
Open this publication in new window or tab >>Lock-free Contention Adapting Search Trees
2018 (English)In: The 30th ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2018, New York, NY, USA, 2018, Vol. 30Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
New York, NY, USA: , 2018
National Category
Computer and Information Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-354022 (URN)10.1145/3210377.3210413 (DOI)978-1-4503-5799-9 (ISBN)
Conference
The 30th ACM Symposium on Parallelism in Algorithms and Architectures, SPAA 2018, July 16–18, 2018, Vienna, Austria
Funder
Swedish Research Council
Note

In press

Available from: 2018-06-18 Created: 2018-06-18 Last updated: 2018-06-27Bibliographically approved
Aronis, S., Jonsson, B., Lång, M. & Sagonas, K. (2018). Optimal dynamic partial order reduction with observers. In: Tools and Algorithms for the Construction and Analysis of Systems: Part II. Paper presented at TACAS 2018, April 14–20, Thessaloniki, Greece. (pp. 229-248). Springer, 10806
Open this publication in new window or tab >>Optimal dynamic partial order reduction with observers
2018 (English)In: Tools and Algorithms for the Construction and Analysis of Systems: Part II, Springer, 2018, Vol. 10806, p. 229-248Conference paper, Published paper (Refereed)
Abstract [en]

Dynamic partial order reduction (DPOR) algorithms are used in stateless model checking (SMC) to combat the combinatorial explosion in the number of schedulings that need to be explored to guarantee soundness. The most effective of them, the Optimal DPOR algorithm, is optimal in the sense that it explores only one scheduling per Mazurkiewicz trace. In this paper, we enhance DPOR with the notion of observability, which makes dependencies between operations conditional on the existence of future operations, called observers. Observers naturally lead to a lazy construction of dependencies. This requires significant changes in the core of POR algorithms (and Optimal DPOR in particular), but also makes the resulting algorithm, Optimal DPOR with Observers, super-optimal in the sense that it explores exponentially less schedulings than Mazurkiewicz traces in some cases. We argue that observers come naturally in many concurrency models, and demonstrate the performance benefits that Optimal DPOR with Observers achieves in both an SMC tool for shared memory concurrency and a tool for concurrency via message passing, using both synthetic and actual programs as benchmarks.

Place, publisher, year, edition, pages
Springer, 2018
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 10806
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-333508 (URN)10.1007/978-3-319-89963-3 _ 14 (DOI)000445822600014 ()978-3-319-89962-6 (ISBN)978-3-319-89963-3 (ISBN)
Conference
TACAS 2018, April 14–20, Thessaloniki, Greece.
Projects
UPMARC
Funder
Swedish Research Council
Available from: 2018-04-14 Created: 2017-11-21 Last updated: 2019-01-07Bibliographically approved
Ngo, T.-P., Abdulla, P., Jonsson, B. & Atig, M. F. (2018). Optimal Stateless Model Checking under the Release-Acquire Semantics. In: SPLASH OOPSLA 2018, Boston, Nov 4-9, 2018: . Paper presented at SPLASH OOPSLA 2018. ACM Digital Library
Open this publication in new window or tab >>Optimal Stateless Model Checking under the Release-Acquire Semantics
2018 (English)In: SPLASH OOPSLA 2018, Boston, Nov 4-9, 2018, ACM Digital Library, 2018Conference paper, Published paper (Refereed)
Abstract [en]

We present a framework for efficient application of stateless model checking (SMC) to concurrent programs running under the Release-Acquire (RA) fragment of the C/C++11 memory model. Our approach is based on exploring the possible program orders, which define the order in which instructions of a thread are executed, and read-from relations, which define how reads obtain their values from writes. This is in contrast to previous approaches, which in addition explore the possible coherence orders, i.e., orderings between conflicting writes. Since unexpected test results such as program crashes or assertion violations depend only on the read-from relation, we avoid a potentially large source of redundancy. Our framework is based on a novel technique for determining whether a particular read-from relation is feasible under the RA semantics. We define an SMC algorithm which is provably optimal in the sense that it explores each program order and read-from relation exactly once. This optimality result is strictly stronger than previous analogous optimality results, which also take coherence order into account. We have implemented our framework in the tool Tracer. Experiments show that Tracer can be significantly faster than state-of-the-art tools that can handle the RA semantics.

Place, publisher, year, edition, pages
ACM Digital Library, 2018
Keywords
Software model checking, C/C++11, Release-Acquire, Concurrent program
National Category
Computer Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-358241 (URN)
Conference
SPLASH OOPSLA 2018
Projects
UPMARC
Available from: 2018-08-26 Created: 2018-08-26 Last updated: 2019-01-09Bibliographically approved
Jonsson, B. (2018). The Quest for Optimality in Stateless Model Checking of Concurrent Programs. In: Howar, F Barnat, J (Ed.), Formal Methods For Industrial Critical Systems, FMICS 2018: . Paper presented at 23rd International Conference on Formal Methods for Industrial Critical Systems (FMICS), SEP 03-04, 2018, Natl Univ Ireland Maynooth, Maynooth, IRELAND (pp. XI-XII). Springer
Open this publication in new window or tab >>The Quest for Optimality in Stateless Model Checking of Concurrent Programs
2018 (English)In: Formal Methods For Industrial Critical Systems, FMICS 2018 / [ed] Howar, F Barnat, J, Springer, 2018, p. XI-XIIConference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer, 2018
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 11119
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-391437 (URN)000477763200001 ()978-3-030-00244-2 (ISBN)978-3-030-00243-5 (ISBN)
Conference
23rd International Conference on Formal Methods for Industrial Critical Systems (FMICS), SEP 03-04, 2018, Natl Univ Ireland Maynooth, Maynooth, IRELAND
Available from: 2019-09-25 Created: 2019-09-25 Last updated: 2019-09-25Bibliographically approved
Abdulla, P., Haziza, F., Holík, L., Jonsson, B. & Rezine, A. (2017). An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures. International Journal on Software Tools for Technology Transfer (STTT), 19(5), 549-563
Open this publication in new window or tab >>An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures
Show others...
2017 (English)In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, Vol. 19, no 5, p. 549-563Article in journal (Refereed) Published
Abstract [en]

We present a technique for automatically verifying safety properties of concurrent programs, in particular programs that rely on subtle dependencies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded number of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state automata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verification, we develop a shape analysis, which tracks correlations between pairs of threads, and a novel abstraction to make the analysis practical. We have implemented our method and used it to verify programs, some of which have not been verified by any other automatic method before.

Place, publisher, year, edition, pages
SPRINGER HEIDELBERG, 2017
Keywords
Verification, Pointer programs, Explicit memory allocation, Queue, Stack, Unbounded, Concurrency, Specification, Linearizability
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:uu:diva-334744 (URN)10.1007/s10009-016-0415-4 (DOI)000409295800004 ()
Available from: 2017-11-29 Created: 2017-11-29 Last updated: 2018-01-13Bibliographically approved
Organisations

Search in DiVA

Show all publications