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

Direct link
BETA
Sagonas, KonstantinosORCID iD iconorcid.org/0000-0001-9657-0179
Publications (10 of 82) Show all publications
Sagonas, K. & Winblad, K. (2018). A contention adapting approach to concurrent ordered sets. Journal of Parallel and Distributed Computing, 115, 1-19
Open this publication in new window or tab >>A contention adapting approach to concurrent ordered sets
2018 (English)In: Journal of Parallel and Distributed Computing, ISSN 0743-7315, E-ISSN 1096-0848, Vol. 115, p. 1-19Article in journal (Refereed) Published
Abstract [en]

With multicores being ubiquitous, concurrent data structures are increasingly important. This article proposes a novel approach to concurrent data structure design where the data structure dynamically adapts its synchronization granularity based on the detected contention and the amount of data that operations are accessing. This approach not only has the potential to reduce overheads associated with synchronization in uncontended scenarios, but can also be beneficial when the amount of data that operations are accessing atomically is unknown. Using this adaptive approach we create a contention adapting search tree (CA tree) that can be used to implement concurrent ordered sets and maps with support for range queries and bulk operations. We provide detailed proof sketches for the linearizability as well as deadlock and livelock freedom of CA tree operations. We experimentally compare CA trees to state-of-the-art concurrent data structures and show that CA trees beat the best of the data structures that we compare against by over 50% in scenarios that contain basic set operations and range queries, outperform them by more than 1200% in scenarios that also contain range updates, and offer performance and scalability that is better than many of them on workloads that only contain basic set operations.

Place, publisher, year, edition, pages
ACADEMIC PRESS INC ELSEVIER SCIENCE, 2018
Keywords
Concurrent data structures, Ordered sets, Linearizability, Range queries
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-351559 (URN)10.1016/j.jpdc.2017.11.007 (DOI)000427809200001 ()
Available from: 2018-05-30 Created: 2018-05-30 Last updated: 2018-06-18Bibliographically 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
Klaftenegger, D., Sagonas, K. & Winblad, K. (2018). Queue Delegation Locking. IEEE Transactions on Parallel and Distributed Systems, 29(3), 687-704
Open this publication in new window or tab >>Queue Delegation Locking
2018 (English)In: IEEE Transactions on Parallel and Distributed Systems, ISSN 1045-9219, E-ISSN 1558-2183, Vol. 29, no 3, p. 687-704Article in journal (Refereed) Published
Abstract [en]

The scalability of parallel programs is often bounded by the performance of synchronization mechanisms used to protect critical sections. The performance of these mechanisms is in turn determined by their sequential execution time, efficient use of hardware, and ability to avoid waiting. In this article, we describe queue delegation (QD) locking, a family of locks that both delegate critical sections and enable detaching execution. Threads delegate work to the thread currently holding the lock and are able to detach, i.e., immediately continue their execution until they need a result from a previously delegated critical section. We show how to use queue delegation to build synchronization algorithms with lower overhead and higher throughput than existing algorithms, even when critical sections need to communicate results back immediately. Experiments when using up to 64 threads to access a shared priority queue show that QD locking provides 10 times higher throughput than Pthreads mutex locks and outperforms leading delegation algorithms. Also, when mixing parallel reads with delegated write operations, QD locking outperforms competing algorithms with an advantage ranging from 9.5 up to 207 percent increased throughput. Last but not least, continuing execution instead of waiting for the execution of critical sections leads to increased parallelism and better scalability. As we will see, queue delegation locking uses simple building blocks whose overhead is low even in uncontended use. All these make the technique useful in a wide variety of applications.

Place, publisher, year, edition, pages
IEEE COMPUTER SOC, 2018
Keywords
Locking, synchronization, delegation, detached execution, multi-core, NUMA
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-348846 (URN)10.1109/TPDS.2017.2767046 (DOI)000425173200015 ()
Available from: 2018-04-20 Created: 2018-04-20 Last updated: 2018-04-20Bibliographically approved
Abdulla, P., Aronis, S., Jonsson, B. & Sagonas, K. (2017). Comparing source sets and persistent sets for partial order reduction. In: Models, Algorithms, Logics and Tools: Essays dedicated to Kim Guldstrand Larsen on the occasion of his 60th birthday (pp. 516-536). Springer
Open this publication in new window or tab >>Comparing source sets and persistent sets for partial order reduction
2017 (English)In: Models, Algorithms, Logics and Tools: Essays dedicated to Kim Guldstrand Larsen on the occasion of his 60th birthday, Springer, 2017, p. 516-536Chapter in book (Other academic)
Place, publisher, year, edition, pages
Springer, 2017
Series
Lecture Notes in Computer Science ; 10460
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-333506 (URN)10.1007/978-3-319-63121-9_26 (DOI)978-3-319-63120-2 (ISBN)
Projects
UPMARC
Available from: 2017-07-25 Created: 2017-11-14 Last updated: 2018-01-13Bibliographically approved
Giantsios, A., Papaspyrou, N. & Sagonas, K. (2017). Concolic testing for functional languages. Science of Computer Programming, 147, 109-134
Open this publication in new window or tab >>Concolic testing for functional languages
2017 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 147, p. 109-134Article in journal (Refereed) Published
Abstract [en]

Concolic testing is a software testing technique that simultaneously combines concrete execution of a program (given specific input, along specific paths) with symbolic execution (generating new test inputs that explore other paths, which gives better path coverage than random test case generation). So far, concolic testing has been applied, mainly at the level of bytecode or assembly code, to programs written in imperative languages that manipulate primitive data types such as integers and arrays. In this article, we demonstrate its application to a functional programming language core, the functional subset of Core Erlang, that supports pattern matching, structured recursive data types such as lists, recursion and higher-order functions. We present CutEr, a tool implementing this testing technique, and describe its architecture, the challenges that it needs to address, its current limitations, and report some experiences from its use.

National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-333909 (URN)10.1016/j.scico.2017.04.008 (DOI)000410014200006 ()
Projects
RELEASE
Funder
Swedish Research Council, 621-2017-04812
Available from: 2017-05-12 Created: 2017-11-18 Last updated: 2018-01-13Bibliographically approved
Trinder, P., Chechina, N., Papaspyrou, N., Sagonas, K., Thompson, S., Adams, S., . . . Winblad, K. (2017). Scaling Reliably: Improving the scalability of the Erlang distributed actor platform. ACM Transactions on Programming Languages and Systems, 39(4), Article ID 17.
Open this publication in new window or tab >>Scaling Reliably: Improving the scalability of the Erlang distributed actor platform
Show others...
2017 (English)In: ACM Transactions on Programming Languages and Systems, ISSN 0164-0925, E-ISSN 1558-4593, Vol. 39, no 4, article id 17Article in journal (Refereed) Published
National Category
Software Engineering
Identifiers
urn:nbn:se:uu:diva-331846 (URN)10.1145/3107937 (DOI)000414328600004 ()
Projects
UPMARCRELEASE
Funder
EU, European Research Council, RII3-CT-2005-026133 IST-2011-287510
Available from: 2017-09-18 Created: 2017-10-18 Last updated: 2018-02-12Bibliographically approved
Asai, K. & Sagonas, K. (2017). Selected and extended papers from Partial Evaluation and Program Manipulation 2015 (PEPM ' 15). Science of Computer Programming, 137, 1-1
Open this publication in new window or tab >>Selected and extended papers from Partial Evaluation and Program Manipulation 2015 (PEPM ' 15)
2017 (English)In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 137, p. 1-1Article in journal, Editorial material (Other academic) Published
Place, publisher, year, edition, pages
ELSEVIER SCIENCE BV, 2017
National Category
Computer and Information Sciences
Identifiers
urn:nbn:se:uu:diva-321558 (URN)10.1016/j.scico.2017.02.001 (DOI)000396972400001 ()
Available from: 2017-05-11 Created: 2017-05-11 Last updated: 2018-01-13Bibliographically approved
Abdulla, P., Aronis, S., Jonsson, B. & Sagonas, K. (2017). Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction. Journal of the ACM, 64(4), Article ID 25.
Open this publication in new window or tab >>Source Sets: A Foundation for Optimal Dynamic Partial Order Reduction
2017 (English)In: Journal of the ACM, ISSN 0004-5411, E-ISSN 1557-735X, Vol. 64, no 4, article id 25Article in journal (Refereed) Published
Abstract [en]

Stateless model checking is a powerful method for program verification that, however, suffers from an exponential growth in the number of explored executions. A successful technique for reducing this number, while still maintaining complete coverage, is Dynamic Partial Order Reduction (DPOR), an algorithm originally introduced by Flanagan and Godefroid in 2005 and since then not only used as a point of reference but also extended by various researchers. In this article, we present a new DPOR algorithm, which is the first to be provably optimal in that it always explores the minimal number of executions. It is based on a novel class of sets, called source sets, that replace the role of persistent sets in previous algorithms. We begin by showing how to modify the original DPOR algorithm to work with source sets, resulting in an efficient and simple-to-implement algorithm, called source-DPOR. Subsequently, we enhance this algorithm with a novel mechanism, called wakeup trees, that allows the resulting algorithm, called optimal-DPOR, to achieve optimality. Both algorithms are then extended to computational models where processes may disable each other, for example, via locks. Finally, we discuss tradeoffs of the source-and optimal-DPOR algorithm and present programs that illustrate significant time and space performance differences between them. We have implemented both algorithms in a publicly available stateless model checking tool for Erlang programs, while the source-DPOR algorithm is at the core of a publicly available stateless model checking tool for C/pthread programs running on machines with relaxed memory models. Experiments show that source sets significantly increase the performance of stateless model checking compared to using the original DPOR algorithm and that wakeup trees incur only a small overhead in both time and space in practice.

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2017
National Category
Software Engineering
Identifiers
urn:nbn:se:uu:diva-331842 (URN)10.1145/3073408 (DOI)000410615900002 ()
Projects
UPMARCRELEASE
Funder
EU, FP7, Seventh Framework Programme, 287510Swedish Research Council
Available from: 2017-10-18 Created: 2017-10-18 Last updated: 2018-01-13Bibliographically 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
Kokologiannakis, M. & Sagonas, K. (2017). Stateless model checking of the Linux kernel's hierarchical read-copy-update (tree RCU). In: Proc. 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software: . Paper presented at SPIN 2017, July 13–14, Santa Barbara, CA (pp. 172-181). New York: ACM Press
Open this publication in new window or tab >>Stateless model checking of the Linux kernel's hierarchical read-copy-update (tree RCU)
2017 (English)In: Proc. 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, New York: ACM Press, 2017, p. 172-181Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
New York: ACM Press, 2017
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-333910 (URN)10.1145/3092282.3092287 (DOI)978-1-4503-5077-8 (ISBN)
Conference
SPIN 2017, July 13–14, Santa Barbara, CA
Projects
UPMARC
Funder
Swedish Research Council, 621-2017-04812
Available from: 2017-07-13 Created: 2017-11-18 Last updated: 2018-01-13Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0001-9657-0179

Search in DiVA

Show all publications