********************************************************************* * Ecole Normale Supe'rieure * * * * Se'minaire * * SEMANTIQUE ET INTERPRETATION ABSTRAITE * * P. Cousot * * * * Vendredi, 14h00--15h30 * * Salle U/V, etage -2 * * DI ENS 45 rue d'Ulm 75005 Paris * ********************************************************************* *** Vendredi 16 avril 2004 *** 14h00 ******************************** Peter O'Hearn (Queen Mary University of London) Resources, Concurrency and Local Reasoning Re'sume': Resource has always been a central concern in concurrent programming. Often, a number of processes share access to system resources such as memory, processor time, or network bandwidth, and correct resource usage is essential for the overall working of a system. In the 1960s and 1970s Dijkstra, Hoare and Brinch Hansen attacked the problem of resource control in their basic works on concurrent programming. In addition to the use of synchronization mechanisms to provide protection from inconsistent use, they stressed the importance of resource separation as a means of controlling the complexity of process interactions and reducing the possibility of time-dependent errors. The intervening years have seen the development of resource-oriented logics such as linear logic and BI. This work uses one such logic, separation logic (a species of BI), to revisit the problem of reasoning about resources in imperative concurrent programs. We use the separating conjunction connective to partition the portions of state used by different processes. The resulting proof method is modular, in the sense that assertions make local remarks about the resources used by program components, instead of global remarks about the entire system state. ********************************************************************* Pour recevoir l'annonce par courrier electronique: cousot@di.ens.fr WWW: http://www.di.ens.fr/~cousot/annonceseminaire.shtml *********************************************************************