Abstrakt. Rely-garanti är en väletablerad metod för att resonera om samtidiga program som använder parallell sammansättning. Parallell sammansättning är dock inte hur samstämmigheten struktureras i verkliga system. Istället startas trådar med "gaffel" och samlas in med "join"-kommandon. Denna typ av samstämmighet kan inte motiveras med att använda förlitan-garanti, eftersom livslängden för en tråd kan avgränsas dynamiskt. Med parallell sammansättning är tillämpningsområdet statiskt. I det här dokumentet introducerar vi argument för förnekande av garantier, en omformulering av förlitan på garantier som gör det möjligt att resonera om dynamiskt spridd samstämmighet. Vi bygger vidare på idéer från separationslogiken för att möjliggöra en dynamisk delning och rekombinering av störningar, på ett liknande sätt som separationslogiken splittrar och förenar högar. För att tillåta denna uppdelning använder vi neka och garantera tillstånd: ett nekat tillstånd anger att miljön inte kan göra en åtgärd, och garantera tillstånd tillåter oss att göra en åtgärd. Vi illustrerar användningen av vårt bevissystem med exempel och visar att det kan koda alla originalsäkerhetsbevis. Vi presenterar också semantiken och sundheten i metoden för förnekande av garantier.
Förnekande-garanti Det finns ett starkt samband mellan vårt arbete och förneka-garanti resonemang REF.
Deny-guarantee reasoning
{'venue': 'In ESOP’09: European Symposium on Programming, volume 5502 of LNCS', 'journal': None, 'mag_field_of_study': ['Computer Science']}