<XML><RECORDS><RECORD><REFERENCE_TYPE>0</REFERENCE_TYPE><REFNUM>7060</REFNUM><AUTHORS><AUTHOR>O'Donnell,J.T.</AUTHOR></AUTHORS><YEAR>1994</YEAR><TITLE>A correctness proof of parallel scan</TITLE><PLACE_PUBLISHED>Parallel Processing Letters, Vol. 4, No. 3 (September 1994) </PLACE_PUBLISHED><PUBLISHER>World Scientific</PUBLISHER><PAGES>329-338</PAGES><LABEL>O'Donnell:1994:7060</LABEL><KEYWORDS><KEYWORD>parallel scan</KEYWORD></KEYWORDS<ABSTRACT>The parallel scan algorithm plays an important role in parallel programming, but previous explanations of it generally rely on informal methods that fail to establish its correctness. Equational reasoning in a pure functional language provides a formal vehicle for stating the parallel scan algorithm and proving that a parallel architecture executes it correctly. The two key ideas in the proof are (1) a collection of lemmas that show how folds and scans can be decomposed into smaller problems, supporting a divide-and-conquer strategy, and (2) a formal specification of the abstract parallel architecture in the same language used to specify the problem, making it possible to reason formally about how the architecture executes the algorithm. </ABSTRACT></RECORD></RECORDS></XML>