Title: Verification of an algorithm for log-time sorting by square comparison
Abstract: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...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).Read More