Previous work Rely-Guarantee (R-G)Method Shared memory concurrency Thread modular verification Only for higher-level code:cobegin/coend a CCAP[Yu&Shao,ICFP'04] The first PCC framework supporting concurrent assembly code R-G method Only support static threads P1l...IPn 2005-9-16 NJPLS@Stevens2005-9-16 NJPLS@Stevens Previous work ◼ Rely-Guarantee (R-G) Method ◼ Shared memory concurrency ◼ Thread modular verification ◼ Only for higher-level code: cobegin/coend ◼ CCAP[Yu&Shao, ICFP’04] ◼ The first PCC framework supporting concurrent assembly code ◼ R-G method ◼ Only support static threads ◼ P1 || … || Pn