Derivation of efficient parallel programs: An example from genetic sequence analysis

Implementation issues such as synchronization, implementation of abstract data types, and scheduling of processes are usually not addressed in the formal derivation of parallel programs. We seek to redress the situation by considering these issues in the context of developing an efficient implementation of an actual parallel program. The computational problem that we proceed by developingan algorithm in Unity and investigating the issues that arise in producing an efficient C implementation of the resulting algorithm. Along the way, we develop some theorems about program refinements, and illustrate the usefulness of the theorems in the context of refining the original Unity program.