Change search
Link to record
Permanent link

Direct link
BETA
Abdulla, Parosh
Alternative names
Publications (10 of 120) Show all publications
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., 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
Abdulla, P. ., Cyriac, A. & Atig, M. F. (2016). Data Communicating Processes with Unreliable Channels. In: Proceedings Of The 31St Annual ACM-IEEE Symposium On Logic In Computer Science (LICS 2016): . Paper presented at 31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS), JUL 05-08, 2016, New York City, NY (pp. 166-175). .
Open this publication in new window or tab >>Data Communicating Processes with Unreliable Channels
2016 (English)In: Proceedings Of The 31St Annual ACM-IEEE Symposium On Logic In Computer Science (LICS 2016), 2016, p. 166-175Conference paper, Published paper (Refereed)
Abstract [en]

We extend the classical model of lossy channel systems by considering systems that operate on a finite set of variables ranging over an infinite data domain. Furthermore, each message inside a channel is equipped with a data item representing its value. Although we restrict the model by allowing the variables to be only tested for (dis-)equality, we show that the state reachability problem is undecidable. In light of this negative result, we consider bounded-phase reachability, where the processes are restricted to performing either send or receive operations during each phase. We show decidability of state reachability in this case by computing a symbolic encoding of the set of system configurations that are reachable from a given configuration.

Keyword
Reachability Problem, Lossy Channel Systems
National Category
Computer Sciences
Identifiers
urn:nbn:se:uu:diva-311415 (URN)10.1145/293355.2934535 (DOI)000387609200017 ()9781450343916 (ISBN)
Conference
31st Annual ACM-IEEE Symposium on Logic in Computer Science (LICS), JUL 05-08, 2016, New York City, NY
Available from: 2016-12-27 Created: 2016-12-27 Last updated: 2018-01-13Bibliographically 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-01-10Bibliographically approved
Abdulla, P. A., Delzanno, G., Rezine, O., Sangnier, A. & Traverso, R. (2016). Parameterized verification of time-sensitive models of ad hoc network protocols. Theoretical Computer Science, 612, 1-22.
Open this publication in new window or tab >>Parameterized verification of time-sensitive models of ad hoc network protocols
Show others...
2016 (English)In: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 612, p. 1-22Article in journal (Refereed) Published
Abstract [en]

We study decidability and undecidability results for parameterized verification of a formal model of timed Ad Hoc network protocols. The communication topology is defined by an undirected graph and the behaviour of each node is defined by a timed automaton communicating with its neighbours via broadcast messages. We consider parameterized verification problems formulated in terms of reachability. In particular we are interested in searching for an initial configuration from which an individual node can reach an error state. We study the problem for dense and discrete time and compare the results with those obtained for (fully connected) networks of timed automata.

Keyword
Parameterized verification, Timed automata, Ad hoc networks, Graphs, Decidability, Well structured transition systems
National Category
Computer Engineering
Identifiers
urn:nbn:se:uu:diva-279630 (URN)10.1016/j.tcs.2015.07.048 (DOI)000369211200001 ()
Available from: 2016-03-08 Created: 2016-03-02 Last updated: 2018-01-10Bibliographically approved
Organisations

Search in DiVA

Show all publications