Att utveckla säkra multitrådade mjukvarusystem är svårt på grund av den potentiella oönskade störningen bland samtidiga trådar. I detta dokument presenteras en flexibel metod för objektorienterade program som skyddar objektstrukturer mot inkonsekvens på grund av rasförhållanden. Den bygger på en ny metod för enkelgängade program där utvecklare definierar aggregerade objektstrukturer med hjälp av ett ägarsystem och deklarerar invarianter över dem. Metoden stöds av en uppsättning språkelement och av både en ljudmodulell statisk verifieringsmetod och stöd för körtidskontroll. I dokumentet redogörs för den preliminära erfarenheten av en prototypimplementering. Ett primärt syfte med ett tillförlitligt programvarusystem är att se till att alla objekt i systemet upprätthåller konsekventa tillstånd: stater där alla fält, och alla fält av andra objekt som de är beroende av, innehåller juridiska meningsfulla värden. I detta dokument formaliserar vi konsekventa begränsningar som objektinvarianter, som bygger på fält. Det är svårt att underhålla objektinvarianter i sekventiella program, och det är ännu svårare i samtidiga program. Tänk till exempel på följande metod: Antag att denna metod är att upprätthålla det invarianta att för alla dual accounts d: I en samtidig inställning kan denna invariant brytas på flera sätt. Även om programmeringssystemet ser till att varje läsning eller skrivande av ett fält är atomär, kan interleavingarna leda till att invarianten kränks. Tänk till exempel på två trådar som båda gör en överföring på samma dubbla konton. Om en överföring sker antingen vid punkt 0 eller 1 under den andra överföringen, då invarianten inte bibehålls. I en samtidig inställning, kan konsekvens av ett objekt säkerställas genom uteslutning på en nivå grövre än enskilda läser och skriver. Till exempel, medan en tråd uppdaterar ett objekt, är det inte tillåtet att utföra någon operation på objektet. I samtida objektorienterade språk genomförs uteslutning via låsning. Garanterad uteslutning förenklar den automatiska verifieringen av multitrådad kod avsevärt. Det innebär att vi helt enkelt kan dela upp beviset för det samtidiga programmet i ett bevis för uteslutning och ett bevis för ett sekventiellt program [24]. I detta dokument presenterar vi en ny programmeringsmetod för flertrådiga objektorienterade program med objektinvarianter. Metoden garanterar inte bara att varje objekt skyddar sig mot konsekvensöverträdelser, utan gör det också möjligt för aggregat av objekt att definiera läckagesäkra ägandedomäner. Dessa domäner garanterar att endast en tråd åt gången kan komma åt ett föremål av aggregatet. Metoden uppnår en sund modulär statisk verifiering genom att kräva att metoderna ska kommenteras med enkla ägandekrav; som ett alternativ ger den också stöd för körtidskontroll som inte kräver några metodanmärkningar. Metoden är en förlängning av Spec#-metoden för sekventiell kod, enligt beskrivningen i vårt tidigare arbete [3]. Vi ser den föreslagna metoden som en grund för en övergripande strategi för specifikation och verifiering av multitrådade program. I det här dokumentet fokuserar vi på den grundläggande säkra metoden för konvergens; vi undersöker också utvidgningar för ökad parallellism och dödlägesförebyggande, men vi anser inte att de som finns i det här dokumentet går vidare enligt följande. De följande fyra avsnitten 1
Jacobs m.fl. REF föreslår en metod för att bevara objektinvarianter i ett parallellt program med finkornig låsmekanism genom ett ägarsystem som stöds av en modulär verifieringsmetod.
Safe concurrency for aggregate objects with invariants
{'venue': "Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)", 'journal': "Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)", 'mag_field_of_study': ['Computer Science']}