| 1. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Consistency and Persistency in Program Verification : Challenges and Opportunities
- 2022
-
Ingår i: Principles of Systems Design. - Cham : Springer. - 9783031223365 - 9783031223372 ; , s. 494-510
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- We consider the verification of concurrent programs and, in particular, the challenges that arise because modern platforms only guarantee weak semantics, i.e., semantics that are weaker than the classical Sequential Consistency (SC). We describe two architectural concepts that give rise to weak semantics, namely weak consistency and weak persistency. The former defines the order in which operations issued by a given process become visible to the rest of the processes. The latter prescribes the order in which data becomes persistent. To deal with the extra complexity in program behaviors that arises due to weak semantics, we propose translating the program verification problem under weak semantics to SC. The main principle is to augment the program with a set of (unbounded) data structures that guarantee the equivalence of the source program’s behavior under the weak semantics with the augmented program’s behavior under the SC semantics. Such an equivalence opens the door to leverage, albeit in a non-trivial manner, the rich set of techniques that we have developed over the years for program verification under the SC semantics. We illustrate the framework’s potential by considering the persistent version of the well-known Total Store Order semantics. We show that we can capture the program behaviors on such a platform using a finite set of unbounded monotone FIFO buffers. The use of monotone FIFO buffers allows the use of the well-structured-systems framework to prove the decidability of the reachability problem.
|
|
| 2. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Deciding Reachability under Persistent x86-TSO
- 2021
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 5
-
Tidskriftsartikel (refereegranskat)abstract
- We address the problem of verifying the reachability problem in programs running under the formal model Px86 defined recently by Raad et al. in POPL'20 for the persistent Intel x86 architecture. We prove that this problem is decidable. To achieve that, we provide a new formal model that is equivalent to Px86 and that has the feature of being a well structured system. Deriving this new model is the result of a deep investigation of the properties of Px86 and the interplay of its components.
|
|
| 3. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Verification under Intel-x86 with Persistency
- 2024
-
Ingår i: Proceedings of the ACM on Programming Languages. - : Association for Computing Machinery (ACM). - 2475-1421. ; 8:PLDI
-
Tidskriftsartikel (refereegranskat)abstract
- The full semantics of the Intel-x86 architecture has been defined by Raad et al in POPL 2022, extending the earlier formalization based on the TSO memory model incorporating persistency. This new semantics involves an intricate combination of the SC, TSO, and PSO models to account for the diverse features of the enlarged instruction set. In this paper we investigate the reachability problem under this semantics, including both its consistency and persistency aspects each of which requires reasoning about unbounded operation reorderings. Our first contribution is to show that reachability under this model can be reduced to reachability under a model without the persistency component. This is achieved by showing that the persistency semantics can be simulated by a finite-state protocol running in parallel with the program. Our second contribution is to prove that reachability under the consistency model of Intel-x86 (even without crashes and persistency) is undecidable. Undecidability is obtained as soon as one thread in the program is allowed to use both TSO variables and two PSO variables. The third contribution is showing that for any fixed bound on the alternation between TSO writes (write-backs), and PSO writes (non-temporal writes), the reachability problem is decidable. This defines a complete parametrized schema for under-approximate analysis that can be used for bug finding.
|
|
| 4. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Verifying Reachability for TSO Programs with Dynamic Thread Creation
- 2022
-
Ingår i: Networked Systems, NETYS 2022. - Cham : Springer. - 9783031174360 - 9783031174353 ; , s. 283-300
-
Konferensbidrag (refereegranskat)abstract
- The verification of reachability properties for programs under weak memory models is a hard problem, even undecidable in some cases. The decidability of this problem has been investigated so far in the case of static programs where the number of threads does not change during execution. However, dynamic thread creation is crucial in asynchronous concurrent programming. In this paper, we address the decidability of the reachability problem for dynamic concurrent programs running under TSO. An important issue when considering a TSO model in this case is maintaining causality precedence between operations issued by threads and those issued by their children. We propose a general TSO model that respects causality and prove that the reachability problem for programs with dynamic creation of threads is decidable.
|
|
| 5. |
- Atig, Mohamed Faouzi, et al.
(författare)
-
Acceleration in Multi-PushDown Systems
- 2016
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer. - 9783662496732 ; , s. 698-714
-
Konferensbidrag (refereegranskat)
|
|
| 6. |
- Atig, Mohamed Faouzi, et al.
(författare)
-
Adjacent ordered multi-pushdown systems
- 2013
-
Ingår i: Developments in Language Theory. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783642387708 ; , s. 58-69
-
Konferensbidrag (refereegranskat)
|
|
| 7. |
|
|
| 8. |
- Atig, Mohamed Faouzi, et al.
(författare)
-
On Bounded Reachability Analysis of Shared Memory Systems
- 2014
-
Ingår i: {IARCS} Annual Conference on Foundations of Software Technology and Theoretical Computer Science, {FSTTCS} 2014, December 15-17, 2014, New Delhi, India.
-
Konferensbidrag (refereegranskat)
|
|
| 9. |
- Atig, Mohamed Faouzi, et al.
(författare)
-
On the Upward/Downward Closures of Petri Nets∗
- 2017
-
Ingår i: 42nd International Symposium on Mathematical Foundations of Computer Science (MFCS 2017). - Dagstuhl, Germany. - 9783959770460 ; , s. 49:1-49:14
-
Konferensbidrag (refereegranskat)abstract
- We study the size and the complexity of computing finite state automata (FSA) representing and approximating the downward and the upward closure of Petri net languages with coverability as the acceptance condition. We show how to construct an FSA recognizing the upward closure of a Petri net language in doubly-exponential time, and therefore the size is at most doubly exponential. For downward closures, we prove that the size of the minimal automata can be non-primitive recursive. In the case of BPP nets, a well-known subclass of Petri nets, we show that an FSA accepting the downward/upward closure can be constructed in exponential time. Furthermore, we consider the problem of checking whether a simple regular language is included in the downward/upward closure of a Petri net/BPP net language. We show that this problem is EXPSPACE-complete (resp. NP-complete) in the case of Petri nets (resp. BPP nets). Finally, we show that it is decidable whether a Petri net language is upward/downward closed.
|
|
| 10. |
- Atig, Mohamed Faouzi, et al.
(författare)
-
Parity Games on Bounded Phase Multi-pushdown Systems
- 2017
-
Ingår i: Networked Systems: 5th International Conference, NETYS 2017, Marrakech, Morocco, May 17-19, 2017, Proceedings. - Cham : Springer International Publishing. - 9783319596471 ; , s. 272-287
-
Konferensbidrag (refereegranskat)abstract
- In this paper we address the problem of solving parity games over the configuration graphs of bounded phase multi-pushdown systems. A non-elementary decision procedure was proposed for this problem by A. Seth. In this paper, we provide a simple and inductive construction to solve this problem. We also prove a non-elementary lower-bound, answering a question posed by A. Seth.
|
|
