Verification of an algorithm for log-time sorting by square comparison
J. C. Mulder, W. P. Weijland · Cambridge University Press eBooks · 1990
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 n 2 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-time 2 =O(n 2 log 4 n ) complexity which is slightly suboptimal with respect to the lower bound of AT 2 = Ω( n 2 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 n 2 -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 n 2 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).