| 1. |
- Abdulla, Parosh Aziz, et al.
(författare)
-
Stateless model checking for TSO and PSO
- 2015
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Berlin, Heidelberg : Springer Berlin/Heidelberg. - 9783662466803 ; , s. 353-367
-
Konferensbidrag (refereegranskat)
|
|
| 2. |
- Abdulla, Parosh, et al.
(författare)
-
Optimal dynamic partial order reduction
- 2014
-
Ingår i: Proc. 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. - New York : ACM Press. - 9781450325448 ; , s. 373-384
-
Konferensbidrag (refereegranskat)abstract
- Stateless model checking is a powerful technique for program verification, which 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). 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, which replace the role of persistent sets in previous algorithms. First, we show how to modify an existing DPOR algorithm to work with source sets, resulting in an efficient and simple to implement algorithm. Second, we extend this algorithm with a novel mechanism, called wakeup trees, that allows to achieve optimality. We have implemented both algorithms in a stateless model checking tool for Erlang programs. Experiments show that source sets significantly increase the performance and that wakeup trees incur only a small overhead in both time and space.
|
|
| 3. |
|
|
| 4. |
- Aronis, Stavros, 1987-, et al.
(författare)
-
A scalability benchmark suite for Erlang/OTP
- 2012
-
Ingår i: Proc. 11th ACM SIGPLAN Workshop on Erlang. - New York : ACM Press. - 9781450315753 ; , s. 33-42
-
Konferensbidrag (refereegranskat)abstract
- Programming language implementers rely heavily on benchmarking for measuring and understanding performance of algorithms, architectural designs, and trade-offs between alternative implementations of compilers, runtime systems, and virtual machine components. Given this fact, it seems a bit ironic that it is often more difficult to come up with a good benchmark suite than a good implementation of a programming language.This paper presents the main aspects of the design and the current status of bencherl, a publicly available scalability benchmark suite for applications written in Erlang. In contrast to other benchmark suites, which are usually designed to report a particular performance point, our benchmark suite aims to assess scalability, i.e., help developers to study a set of performance points that show how an application's performance changes when additional resources (e.g., CPU cores, schedulers, etc.) are added. We describe the scalability dimensions that the suite aims to examine and present its infrastructure and current set of benchmarks. We also report some limited set of performance results in order to show the capabilities of our suite.
|
|
| 5. |
|
|
| 6. |
- Aronis, Stavros, et al.
(författare)
-
Optimal dynamic partial order reduction with observers
- 2018
-
Ingår i: Tools and Algorithms for the Construction and Analysis of Systems. - Cham : Springer. - 9783319899626 - 9783319899633 ; , s. 229-248
-
Konferensbidrag (refereegranskat)abstract
- 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.
|
|
| 7. |
- Aronis, Stavros, 1987-, et al.
(författare)
-
Testing And Verifying Chain Repair Methods For CORFU Using Stateless Model Checking
- 2017
-
Konferensbidrag (refereegranskat)abstract
- Corfu is a distributed shared log that is designed to be scalable and reliable in the presence of failures and asynchrony. Internally, Corfu is fully replicated for fault tolerance, without sharding data or sacrificing strong consistency. In this case study, we present the modeling approaches we followed to test and verify, using Concuerror, the correctness of repair methods for the Chain Replication protocol suitable for Corfu. In the first two methods we tried, Concuerror located bugs quite fast. In contrast, the tool did not manage to find bugs in the third method, but the time this took also motivated an improvement in the tool that reduces the number of traces explored. Besides more details about all the above, we present experiences and lessons learned from applying stateless model checking for verifying complex protocols suitable for distributed programming.
|
|
| 8. |
- Aronis, Stavros, 1987-, et al.
(författare)
-
The shared-memory interferences of Erlang/OTP built-ins
- 2017
-
Ingår i: Proceedings Of The 16Th Acm Sigplan International Workshop On Erlang (Erlang '17). - New York : Association for Computing Machinery (ACM). - 9781450351799 ; , s. 43-54
-
Konferensbidrag (refereegranskat)abstract
- Erlang is a concurrent functional language based on the actor modelof concurrency. In the purest form of this model, actors are realizedby processes that do not share memory and communicate witheach other exclusively via message passing. Erlang comes quiteclose to this model, as message passing is the primary form of interprocesscommunication and each process has its own memoryarea that is managed by the process itself. For this reason, Erlangis often referred to as implementing “shared nothing” concurrency.Although this is a convenient abstraction, in reality Erlang’s mainimplementation, the Erlang/OTP system, comes with a large numberof built-in operations that access memory which is shared byprocesses. In this paper, we categorize these built-ins, and characterizethe interferences between them that can result in observabledifferences of program behaviour when these built-ins are usedin a concurrent setting. The paper is complemented by a publiclyavailable suite of more than one hundred small Erlang programsthat demonstrate the racing behaviour of these built-ins.
|
|
| 9. |
- Asadian, Hooman, et al.
(författare)
-
Applying Symbolic Execution to Test Implementations of a Network Protocol Against its Specification
- 2022
-
Ingår i: 2022 IEEE 15TH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST 2022). - : Institute of Electrical and Electronics Engineers (IEEE). - 9781665466790 - 9781665466806 ; , s. 70-81
-
Konferensbidrag (refereegranskat)abstract
- Implementations of network protocols must conform to their specifications in order to avoid security vulnerabilities and interoperability issues. We describe our experiences using symbolic execution to thoroughly test several implementations of a network security protocol against its specification. We employ a methodology in which we first extract requirements from the protocol's RFC and turn them into formulas. These formulas are then utilized by symbolically executing the protocol implementation to explore code paths that can be traversed on packet sequences that violate a requirement. When this exploration exposes a bug, corresponding input values are produced and turned into test cases that can validate the bug in the original implementation. Since we let symbolic execution be guided by requirements, it can naturally produce a wide variety of requirement-violating input sequences, which is difficult to achieve with existing techniques for protocol testing. We applied this methodology to test four different implementations of MILS against the protocol's RFC. We were able to quickly expose a known CVE in an older version of OpenSSL, and to discover numerous previously unknown vulnerabilities and nonconformance issues in DTI.S implementations, which have by now been confirmed and fixed by their implementors.
|
|
| 10. |
|
|
