Abstrakt. Vi studerar relationen mellan Concurrent Separation Logic (CSL) och antagande-garanti (A-G) metod (alias. Metod för att förlita sig på garantier. Vi visar i tre steg att CSL kan behandlas som en specialisering av A-G-metoden för välsynkroniserade samtidiga program. Först presenterar vi en A-G-baserad programlogik för ett lågnivåspråk med inbyggda låsande primitiver. Sedan utökar vi programlogiken med explicit separation av "privata data" och "delade data", vilket ger bättre minnesmodulalitet. Slutligen visar vi att CSL (anpassad för lågnivåspråket) kan ses som en specialisering av den utvidgade A-G-logiken genom att se till att invarianten att "delade resurser är väl utformade utanför kritiska regioner". Detta arbete kan också ses som ett annat tillvägagångssätt (från Brookes) för att bevisa sundheten i CSL: våra CSL-slutbestämmelser bevisas som lemmas i A-G-baserad logik, vars sundhet är etablerad enligt den syntaktiska metoden för att bevisa sundhet i typsystem.
Konkurrent separation logik kan behandlas som en specialisering av lita-garanti för välsynkroniserade program REF.
On the relationship between concurrent separation logic and assume-guarantee reasoning
{'venue': 'In 16th ESOP', 'journal': None, 'mag_field_of_study': ['Computer Science']}