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

Direct link
BETA
Leonardsson, Carl
Publications (10 of 12) Show all publications
Abdulla, P. A., Atig, M. F., Kaxiras, S., Leonardsson, C., Ros, A. & Zhu, Y. (2018). Mending fences with self-invalidation and self-downgrade. Logical Methods in Computer Science, 14(1), Article ID 6.
Open this publication in new window or tab >>Mending fences with self-invalidation and self-downgrade
Show others...
2018 (English)In: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 14, no 1, article id 6Article in journal (Refereed) Published
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-347675 (URN)000426512000004 ()
Available from: 2018-01-16 Created: 2018-04-06 Last updated: 2018-05-17Bibliographically approved
Ros, A., Leonardsson, C., Sakalis, C. & Kaxiras, S. (2017). Efficient Self-Invalidation/Self-Downgrade for Critical Sections with Relaxed Semantics. IEEE Transactions on Parallel and Distributed Systems, 28(12), 3413-3425
Open this publication in new window or tab >>Efficient Self-Invalidation/Self-Downgrade for Critical Sections with Relaxed Semantics
2017 (English)In: IEEE Transactions on Parallel and Distributed Systems, ISSN 1045-9219, E-ISSN 1558-2183, Vol. 28, no 12, p. 3413-3425Article in journal (Refereed) Published
National Category
Computer Engineering
Identifiers
urn:nbn:se:uu:diva-342215 (URN)10.1109/TPDS.2017.2720744 (DOI)000415179500008 ()
Funder
Swedish Research Council, 621-2012-5332Swedish National Infrastructure for Computing (SNIC)
Available from: 2018-02-20 Created: 2018-02-20 Last updated: 2019-07-03Bibliographically approved
Abdulla, P. A., Aronis, S., Atig, M. F., Jonsson, B., Leonardsson, C. & Sagonas, K. (2017). Stateless model checking for TSO and PSO. Acta Informatica, 54(8), 789-818
Open this publication in new window or tab >>Stateless model checking for TSO and PSO
Show others...
2017 (English)In: Acta Informatica, ISSN 0001-5903, E-ISSN 1432-0525, Vol. 54, no 8, p. 789-818Article in journal (Refereed) Published
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-333902 (URN)10.1007/s00236-016-0275-0 (DOI)000414343200004 ()
Projects
UPMARC
Funder
EU, FP7, Seventh Framework Programme, 287510
Available from: 2016-07-07 Created: 2017-11-18 Last updated: 2018-02-07Bibliographically approved
Ros, A., Leonardsson, C., Sakalis, C. & Kaxiras, S. (2016). Efficient Self-Invalidation/Self-Downgrade for Critical Sections with Relaxed Semantics. In: Proc. International Conference on Parallel Architectures and Compilation: PACT 2016. Paper presented at PACT 2016, September 11–15, Haifa, Israel (pp. 433-434). New York: ACM Press
Open this publication in new window or tab >>Efficient Self-Invalidation/Self-Downgrade for Critical Sections with Relaxed Semantics
2016 (English)In: Proc. International Conference on Parallel Architectures and Compilation: PACT 2016, New York: ACM Press, 2016, p. 433-434Conference paper, Poster (with or without abstract) (Refereed)
Place, publisher, year, edition, pages
New York: ACM Press, 2016
National Category
Computer Engineering
Identifiers
urn:nbn:se:uu:diva-316349 (URN)10.1145/2967938.2974050 (DOI)000392249100042 ()978-1-4503-4121-9 (ISBN)
Conference
PACT 2016, September 11–15, Haifa, Israel
Available from: 2016-09-11 Created: 2017-03-10 Last updated: 2019-07-03Bibliographically approved
Abdulla, P. A., Atig, M. F., Kaxiras, S., Leonardsson, C., Ros, A. & Zhu, Y. (2016). Fencing programs with self-invalidation and self-downgrade. In: Formal Techniques for Distributed Objects, Components, and Systems: . Paper presented at FORTE 2016, June 6–9, Heraklion, Greece (pp. 19-35). Springer
Open this publication in new window or tab >>Fencing programs with self-invalidation and self-downgrade
Show others...
2016 (English)In: Formal Techniques for Distributed Objects, Components, and Systems, Springer, 2016, p. 19-35Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer, 2016
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9688
National Category
Computer Engineering
Identifiers
urn:nbn:se:uu:diva-300663 (URN)10.1007/978-3-319-39570-8_2 (DOI)000379297600002 ()978-3-319-39569-2 (ISBN)
Conference
FORTE 2016, June 6–9, Heraklion, Greece
Projects
UPMARC
Available from: 2016-05-24 Created: 2016-08-10 Last updated: 2018-04-09Bibliographically approved
Sakalis, C., Leonardsson, C., Kaxiras, S. & Ros, A. (2016). Splash-3: A properly synchronized benchmark suite for contemporary research. In: Proc. International Symposium on Performance Analysis of Systems and Software: ISPASS 2016. Paper presented at ISPASS 2016, April 17–19, Uppsala, Sweden (pp. 101-111). IEEE Computer Society
Open this publication in new window or tab >>Splash-3: A properly synchronized benchmark suite for contemporary research
2016 (English)In: Proc. International Symposium on Performance Analysis of Systems and Software: ISPASS 2016, IEEE Computer Society, 2016, p. 101-111Conference paper, Published paper (Refereed)
Abstract [en]

Benchmarks are indispensable in evaluating the performance implications of new research ideas. However, their usefulness is compromised if they do not work correctly on a system under evaluation or, in general, if they cannot be used consistently to compare different systems. A well-known benchmark suite of parallel applications is the Splash-2 suite. Since its creation in the context of the DASH project, Splash-2 benchmarks have been widely used in research. However, Splash-2 was released over two decades ago and does not adhere to the recent C memory consistency model. This leads to unexpected and often incorrect behavior when some Splash-2 benchmarks are used in conjunction with contemporary compilers and hardware (simulated or real). Most importantly, we discovered critical performance bugs that may question some of the reported benchmark results. In this work, we analyze the Splash-2 benchmarks and expose data races and related performance bugs. We rectify the problematic benchmarks and evaluate the resulting performance. Our work contributes to the community a new sanitized version of the Splash-2 benchmarks, called the Splash-3 benchmark suite.

Place, publisher, year, edition, pages
IEEE Computer Society, 2016
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-295418 (URN)10.1109/ISPASS.2016.7482078 (DOI)000382752200010 ()9781509019533 (ISBN)
Conference
ISPASS 2016, April 17–19, Uppsala, Sweden
Projects
UPMARC
Available from: 2016-04-19 Created: 2016-06-07 Last updated: 2019-07-03
Abdulla, P. A., Atig, M. F., Jonsson, B. & Leonardsson, C. (2016). Stateless model checking for POWER. In: Computer Aided Verification: Part II. Paper presented at CAV 2016, July 17–23, Toronto, Canada (pp. 134-156). Springer
Open this publication in new window or tab >>Stateless model checking for POWER
2016 (English)In: Computer Aided Verification: Part II, Springer, 2016, p. 134-156Conference paper, Published paper (Refereed)
Abstract [en]

We present the first framework for efficient application of stateless model checking (SMC) to programs running under the relaxed memory model of POWER. The framework combines several contributions. The first contribution is that we develop a scheme for systematically deriving operational execution models from existing axiomatic ones. The scheme is such that the derived execution models are well suited for efficient SMC. We apply our scheme to the axiomatic model of POWER from [8]. Our main contribution is a technique for efficient SMC, called Relaxed Stateless Model Checking (RSMC), which systematically explores the possible inequivalent executions of a program. RSMC is suitable for execution models obtained using our scheme. We prove that RSMC is sound and optimal for the POWER memory model, in the sense that each complete program behavior is explored exactly once. We show the feasibility of our technique by providing an implementation for programs written in C/pthreads.

Place, publisher, year, edition, pages
Springer, 2016
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9780
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-295424 (URN)10.1007/978-3-319-41540-6_8 (DOI)000387731400008 ()9783319415390 (ISBN)9783319415406 (ISBN)
Conference
CAV 2016, July 17–23, Toronto, Canada
Projects
UPMARC
Available from: 2016-07-13 Created: 2016-06-07 Last updated: 2018-01-10Bibliographically approved
Leonardsson, C. (2016). Verification of Software under Relaxed Memory. (Doctoral dissertation). Uppsala: Acta Universitatis Upsaliensis
Open this publication in new window or tab >>Verification of Software under Relaxed Memory
2016 (English)Doctoral thesis, comprehensive summary (Other academic)
Abstract [en]

The work covered in this thesis concerns automatic analysis of correctness of parallel programs running under relaxed memory models.

When a parallel program is compiled and executed on a modern architecture, various optimizations may cause it to behave in unexpected ways. In particular, accesses to the shared memory may appear in the execution in the opposite order to how they appear in the control flow of the original program source code. The memory model determines which memory accesses can be reordered in a program on a given system. Any memory model that allows some observable memory access reordering is called a relaxed memory model. The reorderings may cause bugs and make the production of parallel programs more difficult.

In this work, we consider three main approaches to analysis of correctness of programs running under relaxed memory models. An exact analysis for finite state programs running under the TSO memory model (Paper I). This technique is based on the well quasi ordering framework. An over-approximate analysis for integer programs running under TSO (Paper II), based on predicate abstraction combined with a buffer abstraction. Two under-approximate analysis techniques for programs running under the TSO, PSO or POWER memory models (Papers III and IV). The latter two techniques are based on stateless model checking and dynamic partial order reduction.

In addition to determining whether a program is correct under a given memory model, the problem of automatic fence synthesis is also considered. A memory fence is an instruction that can be inserted into a program in order to locally disable some memory access reorderings. The fence synthesis problem is the problem of automatically inferring a minimal set of memory fences which restores sufficient order in a given program to ensure its correctness.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2016. p. 102
Series
Digital Comprehensive Summaries of Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1651-6214 ; 1387
Keywords
verification, relaxed memory models
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-297201 (URN)978-91-554-9616-6 (ISBN)
External cooperation:
Public defence
2016-09-07, 2446, Polacksbacken, Lägerhyddsvägen 2, Uppsala, 13:15 (English)
Opponent
Supervisors
Projects
UPMARC
Available from: 2016-08-17 Created: 2016-06-22 Last updated: 2018-01-10
Abdulla, P. A., Aronis, S., Atig, M. F., Jonsson, B., Leonardsson, C. & Sagonas, K. (2015). Stateless model checking for TSO and PSO. In: Baier, Christel; Tinelli, Cesare (Ed.), Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2015. Paper presented at TACAS 2015, April 11–18, London, UK (pp. 353-367). Springer Berlin/Heidelberg
Open this publication in new window or tab >>Stateless model checking for TSO and PSO
Show others...
2015 (English)In: Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2015, Springer Berlin/Heidelberg, 2015, p. 353-367Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2015
Series
Lecture Notes in Computer Science ; 9035
National Category
Software Engineering
Identifiers
urn:nbn:se:uu:diva-251580 (URN)10.1007/978-3-662-46681-0_28 (DOI)978-3-662-46680-3 (ISBN)
Conference
TACAS 2015, April 11–18, London, UK
Projects
UPMARC
Available from: 2015-04-21 Created: 2015-04-21 Last updated: 2018-01-11Bibliographically approved
Abdulla, P. A., Atig, M. F., Chen, Y.-F., Leonardsson, C. & Rezine, A. (2013). MEMORAX, a Precise and Sound Tool for Automatic Fence Insertion under TSO. In: Piterman, Nir; Smolka, ScottA. (Ed.), Tools and Algorithms for the Construction and Analysis of Systems: . Paper presented at 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, March 16-24, 2013, Rome, Italy (pp. 530-536). Springer Berlin/Heidelberg
Open this publication in new window or tab >>MEMORAX, a Precise and Sound Tool for Automatic Fence Insertion under TSO
Show others...
2013 (English)In: Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin/Heidelberg, 2013, p. 530-536Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer Berlin/Heidelberg, 2013
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 7795
National Category
Software Engineering
Identifiers
urn:nbn:se:uu:diva-203169 (URN)10.1007/978-3-642-36742-7_37 (DOI)978-3-642-36741-0 (ISBN)
Conference
19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, March 16-24, 2013, Rome, Italy
Projects
UPMARCWeak Memory Models
Available from: 2013-07-03 Created: 2013-07-03 Last updated: 2018-01-11Bibliographically approved
Organisations

Search in DiVA

Show all publications