Edited by J. C. M. Baeten
Publisher: Cambridge University Press
Print Publication Year: 1990
Online Publication Date:December 2009
Online ISBN:9780511608841
Hardback ISBN:9780521400282
Paperback ISBN:9780521607506
Chapter DOI: http://dx.doi.org/10.1017/CBO9780511608841.008
Subjects: Programming Languages and Applied Logic, Distributed, Networked and Mobile Computing
Image View Extract Fullview: Text View | Enlarge Image ‹ Previous Chapter ›Next Chapter
In this paper a concurrent sorting algorithm called ranksort is presented, able to sort an input sequence of length n in log n time, using n2 processors. The algorithm is formally specified as a delay-insensitive circuit. Then, a formal correctness proof is given, using bisimulation semantics in the language ACPτ. The algorithm has area-time2=O(n2 log4n) complexity which is slightly suboptimal with respect to the lower bound of AT2 = Ω(n2 log n).
INTRODUCTION
Many authors have studied the concurrency aspects of sorting, and indeed the n-time bubblesort algorithm (using n processors) is rather thoroughly analyzed already (e.g. see: Hennessy, Kossen and Weijland). However, bubblesort is not the most efficient sorting algorithm in sequential programming, since it is n2-time and for instance heapsort and mergesort are n log n-time sorting algorithms. So, the natural question arises whether it would be possible to design an algorithm using even less than n-time.
In this paper we discuss a concurrent algorithm, capable of sorting n numbers in O(log n) time. This algorithm is based on the idea of square comparison: putting all numbers to be sorted in a square matrix, all comparisons can be made in O(1) time, using n2 processors (one for each cell of the matrix). Then, the algorithm only needs to evaluate the result of this operation.
The algorithm presented here, which is called ranksort, is not the only concurrent time-efficient sorting algorithm. Several sub n-time algorithms have been developed by others (see: Thompson).
pp. i-iv
pp. v-x
pp. xi-xii
An introduction to process algebra : Read PDF
pp. 1-22
Two simple protocols : Read PDF
pp. 23-44
Proving mutual exclusion with process algebra : Read PDF
pp. 45-52
Process algebra as a tool for the specification and verification of CIM-architectures : Read PDF
pp. 53-80
A process creation mechanism in process algebra : Read PDF
pp. 81-88
Correctness proofs for systolic algorithms: palindromes and sorting : Read PDF
pp. 89-126
Verification of an algorithm for log-time sorting by square comparison : Read PDF
pp. 127-146
On the Amoeba protocol : Read PDF
pp. 147-172
Process algebra semantics of POOL : Read PDF
pp. 173-236
Some observations on redundancy in a context : Read PDF
pp. 237-260
A modular approach to protocol verification using process algebra : Read PDF
pp. 261-306
pp. 307-312
pp. 313-316
Index of symbols and notation : Read PDF
pp. 317-317