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 85) 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
Löscher, A. & Sagonas, K. (2018). Automating Targeted Property-Based Testing. In: IEEE 11th International Conference on Software Testing, Verification and Validation (ICST): . Paper presented at 11th IEEE International Conference on Software Testing, Verification and Validation (ICST), APR 09-13, 2018, Vasteras, SWEDEN (pp. 70-80). IEEE
Open this publication in new window or tab >>Automating Targeted Property-Based Testing
2018 (English)In: IEEE 11th International Conference on Software Testing, Verification and Validation (ICST), IEEE , 2018, p. 70-80Conference paper, Published paper (Refereed)
Abstract [en]

Targeted property-based testing is an enhanced form of property-based testing (PBT) where the input generation is guided by a search strategy instead of being random, thereby combining the strengths of QuickCheck-like and search-based testing techniques. To use it, however, the user currently needs to specify a search strategy and also supply all ingredients that the search strategy requires. This is often a laborious process and makes targeted PBT less attractive than its random counterpart. In this paper, we focus on simulated annealing, the default search strategy of our tool, and present a technique that automatically creates all the ingredients that targeted PBT requires starting from only a random generator. Our experiments, comparing the automatically generated ingredients to fine-tuned manually written ones, show that the performance that one obtains is sufficient and quite competitive in practice.

Place, publisher, year, edition, pages
IEEE, 2018
Series
IEEE International Conference on Software Testing Verification and Validation, ISSN 2381-2834
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-365885 (URN)10.1109/ICST.2018.00017 (DOI)000435006300007 ()978-1-5386-5012-7 (ISBN)
Conference
11th IEEE International Conference on Software Testing, Verification and Validation (ICST), APR 09-13, 2018, Vasteras, SWEDEN
Funder
Swedish Foundation for Strategic Research Swedish Research Council
Available from: 2018-11-20 Created: 2018-11-20 Last updated: 2018-11-20Bibliographically 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
Sagonas, K. (2018). Progress on Algorithms for Stateless Model Checking. Paper presented at Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation Thessaloniki, Greece, 20th April 2018. Electronic Proceedings in Theoretical Computer Science (268), Article ID Preface.
Open this publication in new window or tab >>Progress on Algorithms for Stateless Model Checking
2018 (English)In: Electronic Proceedings in Theoretical Computer Science, ISSN 2075-2180, E-ISSN 2075-2180, no 268, article id PrefaceArticle in journal, Editorial material (Other academic) Published
Place, publisher, year, edition, pages
OPEN PUBL ASSOC, 2018
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-364845 (URN)10.4204/EPTCS.268 (DOI)000444023000003 ()
Conference
Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation Thessaloniki, Greece, 20th April 2018
Available from: 2018-11-06 Created: 2018-11-06 Last updated: 2018-11-06Bibliographically 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)
Abstract [en]

Partial order reduction has traditionally been based on persistent sets, ample sets, stubborn sets, or variants thereof. Recently, we have presented a strengthening of this foundation, using source sets instead of persistent/ample/stubborn sets. Source sets subsume persistent sets and are often smaller than persistent sets. We introduced source sets as a basis for Dynamic Partial Order Reduction (DPOR), in a framework which assumes that processes are deterministic and that all program executions are finite. In this paper, show how to use source sets for partial order reduction in a framework which does not impose these restrictions. We also compare source sets with persistent sets, providing some insights into conditions under which source sets and persistent sets do or do not differ.

Place, publisher, year, edition, pages
Springer, 2017
Series
Lecture Notes in Computer Science, E-ISSN 1611-3349 ; 10460
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-333506 (URN)10.1007/978-3-319-63121-9_26 (DOI)000441452500026 ()978-3-319-63120-2 (ISBN)978-3-319-63121-9 (ISBN)
Projects
UPMARC
Funder
Swedish Research Council
Available from: 2017-07-25 Created: 2017-11-14 Last updated: 2018-11-09Bibliographically 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
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0001-9657-0179

Search in DiVA

Show all publications