The meaning of concurrent programs

system during a single processor cycle. But we can abstract out properties of the sequences and focus on the properties of interest. The "specifications" given here are in ordinary working mathematical notation plus some relatively informal language. I have made a deliberate effort to try to avoid unnecessary formalization. A statement of the form "at this state "x" holds contents = j" is clear enough -- and can be translated into more formal mathematical notation whenever needed. See section 3 for details. On the other hand, I have made efforts to avoid oversimplifying the semantics of actual computations. For example, the execution of an atomic "compare and swap" operation is both impressively complex and precise. When a thread reaches the start of this operation, there may be interrupts which cause unspecified delays as the operating system switches out the thread and any number of other tasks may start the same operation "at the same tim...

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Victor Yodaiken
• Keywords: CORR 2008, Education, Formal Mathematical Notation, Mathematical Notation, Single Processor Cycle