Change search
Link to record
Permanent link

Direct link
BETA
Abdulla, Parosh
Alternative names
Publications (10 of 123) Show all publications
Abdulla, P. A., Atig, M. F., Bouajjani, A. & Ngo, T. P. (2018). A load-buffer semantics for total store ordering. Logical Methods in Computer Science, 14(1), Article ID 9.
Open this publication in new window or tab >>A load-buffer semantics for total store ordering
2018 (English)In: Logical Methods in Computer Science, ISSN 1860-5974, E-ISSN 1860-5974, Vol. 14, no 1, article id 9Article in journal (Refereed) Published
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-337278 (URN)000426512000008 ()
Projects
UPMARC
Available from: 2018-01-23 Created: 2017-12-21 Last updated: 2018-05-17Bibliographically approved
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
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
Keyword
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
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
Abdulla, P. A., Atig, M. F., Bouajjani, A. & Ngo, T. P. (2017). Context-bounded analysis for POWER. In: Tools and Algorithms for the Construction and Analysis of Systems: Part II. Paper presented at TACAS 2017, April 22–29, Uppsala, Sweden (pp. 56-74). Springer
Open this publication in new window or tab >>Context-bounded analysis for POWER
2017 (English)In: Tools and Algorithms for the Construction and Analysis of Systems: Part II, Springer, 2017, p. 56-74Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer, 2017
Series
Lecture Notes in Computer Science ; 10206
National Category
Computer Systems
Identifiers
urn:nbn:se:uu:diva-314901 (URN)10.1007/978-3-662-54580-5_4 (DOI)978-3-662-54579-9 (ISBN)
Conference
TACAS 2017, April 22–29, Uppsala, Sweden
Projects
UPMARC
Available from: 2017-03-31 Created: 2017-02-07 Last updated: 2017-05-02Bibliographically approved
Abdulla, P. A., Atig, M. F., Chen, Y.-F., Bui, P. D., Holık, L., Rezine, A. & Rümmer, P. (2017). Flatten and Conquer: A Framework for Efficient Analysis of String Constraints. Paper presented at 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Barcelona, June 18-23, 2017. SIGPLAN notices, 52(6), 602-617
Open this publication in new window or tab >>Flatten and Conquer: A Framework for Efficient Analysis of String Constraints
Show others...
2017 (English)In: SIGPLAN notices, ISSN 0362-1340, E-ISSN 1558-1160, Vol. 52, no 6, p. 602-617Article in journal (Refereed) Published
Abstract [en]

We describe a uniform and efficient framework for checking the satisfiability of a large class of string constraints. The framework is based on the observation that both satisfiability and unsatisfiability of common constraints can be demonstrated through witnesses with simple patterns. These patterns are captured using flat automata each of which consists of a sequence of simple loops. We build a Counter-Example Guided Abstraction Refinement (CEGAR) framework which contains both an under-and an over-approximation module. The flow of information between the modules allows to increase the precision in an automatic manner. We have implemented the framework as a tool and performed extensive experimentation that demonstrates both the generality and efficiency of our method.

National Category
Engineering and Technology
Identifiers
urn:nbn:se:uu:diva-328181 (URN)10.1145/3062341.3062384 (DOI)000414334200041 ()978-1-4503-4988-8 (ISBN)
Conference
38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Barcelona, June 18-23, 2017
Available from: 2017-08-18 Created: 2017-08-18 Last updated: 2018-03-20Bibliographically 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
Abdulla, P., Jonsson, B. & Trinh, C. Q. (2016). Automated Verification of Linearization Policies. In: Automated Verification of Linearization Policies: 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings. Paper presented at 23rd International Symposium, SAS 2016.
Open this publication in new window or tab >>Automated Verification of Linearization Policies
2016 (English)In: Automated Verification of Linearization Policies: 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, 2016Conference paper, Published paper (Other academic)
Abstract [en]

We present a novel framework for automated verification of linearizability for concurrent data structures that implement sets, stacks, and queues. The framework requires the user to provide a linearization policy, which describes how linearization point placement in different concurrent threads affect each other; such linearization policies are often provided informally together with descriptions of new algorithms. We present a specification formalism for linearization policies which allows the user to specify, in a simple and concise manner, complex patterns including non-fixed linearization points. To automate verification, we extend thread-modular reasoning to bound the number of considered threads, and use a novel symbolic representation for unbounded heap structures that store data from an unbounded domain. We have implemented our framework in a tool and successfully used it to prove linearizability for a wide range of algorithms, including all implementations of concurrent sets, stacks, and queues based on singly-linked lists that are known to us from the literature.

National Category
Computer Systems
Research subject
Computer Science
Identifiers
urn:nbn:se:uu:diva-305226 (URN)10.1007/978-3-662-53413-7_4 (DOI)000388924600004 ()9783662534120 (ISBN)9783662534137 (ISBN)
Conference
23rd International Symposium, SAS 2016
Available from: 2016-10-13 Created: 2016-10-13 Last updated: 2017-01-02Bibliographically approved
Abdulla, P. A., Atig, M. F. & Bui, P. D. (2016). Counter-Example Guided Program Verification. In: FM 2016: Formal Methods. Paper presented at FM 2016, November 9-11, Limassol, Cyprus (pp. 25-42). Springer
Open this publication in new window or tab >>Counter-Example Guided Program Verification
2016 (English)In: FM 2016: Formal Methods, Springer, 2016, p. 25-42Conference paper, Published paper (Refereed)
Place, publisher, year, edition, pages
Springer, 2016
Series
Lecture Notes in Computer Science, ISSN 0302-9743 ; 9995
National Category
Computer Systems
Identifiers
urn:nbn:se:uu:diva-307789 (URN)10.1007/978-3-319-48989-6_2 (DOI)000389793300002 ()978-3-319-48988-9 (ISBN)
Conference
FM 2016, November 9-11, Limassol, Cyprus
Available from: 2016-11-08 Created: 2016-11-21 Last updated: 2017-02-10Bibliographically approved
Organisations

Search in DiVA

Show all publications