Formal derivation of concurrent assignments from scheduled single assignments

Lisper, Björn (1991) Formal derivation of concurrent assignments from scheduled single assignments. [SICS Report]



Concurrent assignments are commonly used to describe synchronous parallel computations. We show how a sequence of concurrent assignments can be formally derived from the schedule of an acyclic single assignment task graph and a memory allocation. In order to do this we develop a formal model of memory allocation in synchronous systems. We use weakest precondition semantics to show that the sequence of concurrent assignments computes the same values as the scheduled single assignments. We give a lower bound on the memory requirements of memory allocations for a given schedule. This bound is tight: we define a class of memory allocations whose memory requirements always meets the bound. This class corresponds to conventional register allocation for DAGs and is suitable when memory access times are uniform. We furthermore define a class of simple ``shift register'' memory allocation. These allocations have the advantage of a minimum of explicit storage control and they yield local or nearest-neighbour accesses in distributed systems whenever the schedule allows this. Thus, this class of allocations is suitable when designing parallel special-purpose hardware, like systolic arrays.

Item Type:SICS Report
ID Code:2104
Deposited By:Vicki Carleson
Deposited On:23 Oct 2009
Last Modified:18 Nov 2009 16:00

Repository Staff Only: item control page