MRTC publications
|
Two Formal Semantics for PLEX |
||||||
|
||||||
|
Abstract In any system with shared data and concurrent (or independent) activities, there is a need to guarantee exclusive access to the shared data. If the independent parts are executed in a non-preemptive fashion, on a single-processor architecture, the exclusive access is automatically guaranteed. The problem arises when the single-processor architecture is to be replaced by a multi-processor ditto; different parts, still executed in a non-preemptive fashion, but on different processors, may now access and update the same data concurrently. Since re-implementation is an infeasible solution for a legacy system, which usually contains several million lines of code, there is a need for criteria that can ensure when functional equivalence, in some central aspect, is preserved for parallel execution of the software. To ensure the correctness of these criteria, the formal semantics of the language in question has to be considered. The AXE telephone exchange system from Ericsson exposes the above properties: independent activities, shared data, non-preemptive execution, and a single-processor architecture. PLEX is used to program the functionality in the system, and in this paper we develop an operational semantics for the current single-processor architecture, as well as for an experimental multi-threaded, shared-memory, architecture. |
||||||
|
BibTeX entry @inproceedings{Lindhult_0964:2005, |
- Mälardalen University |
- Box 883 |
- 721 23 Västerås/Eskilstuna |
- 021-101300, 016-153600 |
- webmaster |
- Latest update: 2012.08.24