Design and implementation of Parallel TRAM. Algebraic specifications, introduced in the mid 70’s as a method of modeling and specifying abstract data types, has been widely attracting attention since they have exact semantics and the ability to verify and reason about specifications of software systems. In addition, since specifications written in algebraic specification languages can be executed on stock hardware, the specification languages can be used as tools for rapid prototyping. TRAM is an abstract machine for order-sorted conditional term rewritting systems (OSCTRSs). The OSCTRSs can serve as a general computation model for advanced algebraic specification languages such as OBJ and CafeOBJ. TRAM adopts the E-strategy as its reduction strategy. Parallel TRAM is a parallel variant of TRAM that is designed to be executed on shared-memory multiprocessors. In Parallel TRAM, parallelism directives are specified by using the Parallel E-strategy that is an extension of the E-strategy. The Parallel E-strategy may control parallelism suitably by combining conditions. In this paper, we describe the design and implementation of Parallel TRAM and assess the current implementation on OMRON LUNA-88K 2 .
Keywords for this software
References in zbMATH (referenced in 2 articles , 1 standard article )
Showing results 1 to 2 of 2.
- Ogata, Kazuhiro; Futatsugi, Kokichi: Theorem proving based on proof scores for rewrite theory specifications of otss (2014)
- Ogata, Kazuhiro; Kondo, Masaru; Ioroi, Shigenori; Futatsugi, Kokichi: Design and implementation of Parallel TRAM (1997)