Abstract
========
Most methods for reasoning about concurrent programs, both formal and informal, assume sequential consistency. This assumption, however, is not valid in modern systems which satisfy a weaker memory model. Fortunately, most memory models have the property that if a program is free of data races (precisely defined) in sequentially consistent executions, then its behavior will be the same as if its execution were sequentially consistent, thus allowing established methods for reasoning about the program to be soundly employed. It is the responsibility of the programmer to ensure that there are no data races in the program by using synchronization appropriately, marking variables volatile, etc. In this talk, I will describe an approach to verifying that a program is free from data races using assertional reasoning based on weakest preconditions. A proof of data-race freedom can utilize invariants and other inferred or programmer provided assertions. This approach is general and can deal with more valid programming idioms than other approaches to detecting data races that look for satisfaction of derived conditions such as conformance to a locking protocol.