Verification of an algorithm for log-time sorting by square comparison  pp. 127-146

Verification of an algorithm for log-time sorting by square comparison

By J. C. Mulder and W. P. Weijland

Image View 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).