parallel_reorder.pvl

class ParReorder {
	//ghost variables
	given int[] prefixsumCopy;
	//function invariants
	context_everywhere input != null && output != null && partialInput != null && prefixsum != null;
	context_everywhere radix > 1;
	context_everywhere input.length == output.length && input.length == partialInput.length;
	context_everywhere prefixsum.length == radix + 1;
	//permission specifications
	context (\forall* int i; i >= 0 && i < input.length; Perm(input[i], read));
	context (\forall* int i; i >= 0 && i < partialInput.length; Perm(partialInput[i], read));
	context (\forall* int i; i >= 0 && i < output.length; Perm(output[i], write));
	context (\forall* int i; i >= 0 && i < prefixsum.length; Perm(prefixsum[i], write));
	//preconditions
	requires prefixsum[prefixsum.length - 1] == input.length;
	requires (\forall int i; i >= 0 && i < prefixsum.length;
		(\forall int j; j >= 0 && j < prefixsum.length; i >= j ==> prefixsum[i] >= prefixsum[j]));
	requires (\forall int i; i >= 0 && i < prefixsum.length; prefixsum[i] >= 0 && prefixsum[i] < output.length);
	void parReorder(int radix, int[] partialInput, int[] input, int[] output, int[] prefixsum) {
		
		par reorder(int tid = 0..radix)
		//ghost variables
		context prefixsum == prefixsumCopy;
		//permission specifications
		requires Perm(prefixsum[tid], write);
		requires Perm(prefixsumCopy[tid], read);
		requires Perm(prefixsumCopy[tid + 1], read);
		requires (\forall* int i; i >= 0 && i < input.length; Perm(input[i], read));
		requires (\forall* int i; i >= 0 && i < partialInput.length; Perm(partialInput[i], read));
		requires (\forall* int i; i >= prefixsumCopy[tid] && i < prefixsumCopy[tid + 1]; Perm(output[i], write));
		{
			loop_invariant Perm(prefixsum[tid], write);
			loop_invariant Perm(prefixsumCopy[tid], read);
			loop_invariant Perm(prefixsumCopy[tid + 1], read);
			loop_invariant (\forall* int i; i >= 0 && i < input.length; Perm(input[i], read));
			loop_invariant (\forall* int i; i >= 0 && i < partialInput.length; Perm(partialInput[i], read));
			loop_invariant (\forall* int i; i >= prefixsumCopy[tid] && i < prefixsumCopy[tid + 1]; Perm(output[i], write));
			for(int i = 0; i < partialInput.length; i++) {
				if(partialInput[i] == tid) {
					output[prefixsum[tid]] = input[i];
					prefixsum[tid] = prefixsum[tid] + 1;
				}
			}
		}
	}
}