A mechanically certified theorem about optimal concurrency of sorting networks

1 January 1986

proceedings article
Published by Association for Computing Machinery (ACM)

p. 307-317
https://doi.org/10.1145/512644.512673

Abstract

Our concern is the mechanical certification of transformations of sequential program executions into parallel executions with equivalent semantics. The objective of such transformations is to accelerate the execution of programs. The result reported here is a mechanically certified theorem of optimality. We present a transformation which applies to every program in a particular programming language, the language of sorting networks. This transformation transforms the sequential execution of any sorting network into an execution which is as fast or faster than any other transformation which applies to every sorting network. The theorem is stated formally in a mechanized logic.

Keywords

PARTICULAR PROGRAMMING LANGUAGE
PARALLEL EXECUTION
MECHANICAL CERTIFICATION
CERTIFIED THEOREM
OPTIMAL CONCURRENCY
SEQUENTIAL PROGRAM EXECUTION
MECHANIZED LOGIC
SEQUENTIAL EXECUTION
EQUIVALENT SEMANTICS
SORTING NETWORK

This publication has 0 references indexed in Scilit: