Abstract-Transactional Memory (TM) är en lovande teknik som tar itu med svårigheten med parallell programmering. Eftersom TM tar ansvar för all konvergenskontroll är TM-systemen mycket sårbara för subtila korrekthetsfel. På grund av svårigheten att till fullo bevisa riktigheten i TM-system, många av dem används utan några formella korrekthetsgarantier. I detta dokument presenteras ChkTM, en flexibel modellkontrollmiljö för att verifiera att olika TM-system är korrekta. ChkTM syftar till att modellera TM-system nära genomförandenivån för att avslöja så många potentiella fel som möjligt. ChkTM modellerar till exempel exakt versionskontrollmekanismen i tidsstämpelbaserad programvara TMs (STMs). Dessutom kan ChkTM flexibelt modellera TM-system som använder ytterligare hårdvarukomponenter eller stöder nästintill parallellism. Med hjälp av ChkTM modellerar vi flera TM-system, inklusive en brett använd industriell STM (TL2), en hybrid TM (SigTM) som använder hårdvarusignaturer, och en STM (NesTM) som stöder inbäddade parallella transaktioner. Vi visar sedan hur ChkTM kan användas för att hitta en tidigare orapporterad felkorrektur i den aktuella implementeringen av iver-version TL2. Vi verifierar även serialiseringen av TL2 och SigTM samt starka isoleringsgarantier för SigTM. Slutligen analyserar vi kvantitativt ChkTM för att förstå de praktiska frågorna och motivera ytterligare forskning i modellkontroll TM-system.
Baek på al. REF presenterar ChkTM, en modellkontrollmiljö som kan verifiera att transaktionsminnen är korrekta.
Implementing and Evaluating a Model Checker for Transactional Memory Systems
{'venue': '2010 15th IEEE International Conference on Engineering of Complex Computer Systems', 'journal': '2010 15th IEEE International Conference on Engineering of Complex Computer Systems', 'mag_field_of_study': ['Computer Science']}