The automated proof of a trace transformation for a bitonic sort

DOI10.1016/0304-3975(86)90033-2MaRDI QIDQ1822503zbMATH OpenOpenAlexFDO

Authors Chua-Huang Huang, Christian Lengauer

Publication date 1986

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(86)90033-2

zbMATH Keywords

bitonic sortingconcurrencystepwise refinement

Mathematics Subject Classification ID

Searching and sorting (68P10) Analysis of algorithms and problem complexity (68Q25) Specification and verification (program logics, model checking, etc.) (68Q60)

Review text

In his third volume of The Art of Computer Programming (1973; Zbl 0302.68010), \textit{D. E. Knuth} presents Batcher's bitonic sorting network. With concurrency, this sorting network can be executed in logarithmic time. Knuth suggests a formal argument for the correctness of the bitonic sorting algorithm (as an exercise), but addresses the question of concurrency only informally. We develop a program for the bitonic sort by (1) deriving a stepwise refinement from Knuth's informal description of the algorithm, (2) deriving from the refinement a sequential execution or 'trace' of order O(n log n) in the length n of the sequence to be sorted, and (3) transforming the sequential trace into a parallel trace of order O(log n) while preserving its semantics. We shall be informal in Steps 1 and 2 - although these steps can be formalized. But we will provide a formal treatment of Step 3 and report on the certification of this treatment in a mechanized logic. This work is a contribution to the optimization of programs (via concurrency) through transformation and the automation of program proofs.

Recommendations

• On the role of automated theorem proving in the compile-time derivation of concurrency
• On optimal parallelization of sorting networks
• A note on bitonic sorting
• Automatic Parallelization and Optimization of Programs by Proof Rewriting
• Types for Proofs and Programs

Cites work

• A methodology for programming with concurrency: An informal presentation
• A methodology for programming with concurrency: The formalism
• Automatic program verification. I: A logical basis and its implementation
• Compiler specification and verification
• scientific article; zbMATH DE number 4164171 (Why is no real title available?)
• scientific article; zbMATH DE number 3902008 (Why is no real title available?)
• scientific article; zbMATH DE number 3473265 (Why is no real title available?)
• Mechanical proofs about computer programs
• On the role of automated theorem proving in the compile-time derivation of concurrency
• Programming as a Discipline of Mathematical Nature

Cited in

(7)

• A note on bitonic sorting
• Odd-even sort in powerlists
• Parallelization of divide-and-conquer in the Bird-Meertens formalism
• scientific article; zbMATH DE number 3902008 (Why is no real title available?)
• Types for Proofs and Programs
• A theorem prover for a computational logic
• On optimal parallelization of sorting networks

Describes a project that uses

Uses Software

• NQTHM

This page was built for publication: The automated proof of a trace transformation for a bitonic sort

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1822503)