The multicore revolution of the early 21st century has introduced a multitude of multiprocessor synchronization techniques for designing concurrent data structures. This thesis explores the concept of “unrolling”, or storing multiple data items per node, in order to increase the concurrent throughput of linked-lists, or more specifically list-based sets of linked nodes. Our contribution is a concurrent unrolled list-based set implemented in the Java programming language which uses lock-based lazy synchronization with memory management handled by the Java Virtual Machine (JVM). Our unrolled list implementation provides decreased traversal overhead over the state-of-the-art concurrent linked lists under limited contention, along with improved spatial locality due to unrolled node data items being stored in sequential memory locations. Our results show that in comparison to the state-of-the- art lock-based and lock-free concurrent list-based set implementations in Java, our concurrent unrolled list-based set provides between 1.7x to 12.2x increased concurrent throughput under medium contention, and 25.7x to 196.5x increased concurrent throughput under low contention, depending on the ratio of write to read operations. Furthermore, we show that unrolling a concurrent linked-list can provide at least 60% of the performance of the Java concurrency package’s native lock-free skiplist, namely ConcurrentSkipListSet. / Den revolutionerande utvecklingen av flerkärniga processorer under början av 2000-talet har medfört många nya designprinciper för samverkande datastrukturer. Den här avhandlingen behandlar utrullings-konceptet eller hur man lagrar multipla dataenheter per nod för att kunna öka genomströmningen av länkade listor, eller mer specifikt listor bestående av länkade noder. Vårt bidrag består av samverkande list-baserade set implementerade i programmeringsspråket Java som använder låsbaserad lat synkronisering där JVM (Java Virtual Machine) hanterar minnet. Vår implementering av utrullade listor ger minskad tvärgående overhead över toppmoderna samverkande länkade listor med reducerad kapacitetsbegränsning, och med förbättrad plats eftersom utrullade datanoder sparas på sekventiella minnesplatser. Våra resultat visar att, i jämförelse med andra toppmoderna låsta och låsfria samverkande listbaserade set i Java, ger vår implementation mellan 1.7 till 12.2 gånger mer genomströmning under normal kapacitetsbegränsning och med 25.7 till 196.5 under låg kapacitetsbegränsning, beroende på graden av skriv- och läsprocesser. Vidare visar vi att en utrullad samverkande länkad lista kan ge minst 60% bättre prestanda i Javas paket för låsfria samverkande listor kallad ConcurrentSkipListSet.

Cieľom tejto práce je návrh analýzy tvaru haldy vhodnej pre potreby analyzátora 2LS. 2LS je nástroj pre analýzu C programov založený na automatickom odvodzovaní invariantov s použitím SMT solvera. Navrhované riešenie obsahuje spôsob reprezentácie tvaru programovej haldy pomocou logických formulí nad teóriou bitových vektorov. Tie sú následne využité v SMT solveri pre predikátovú logiku prvého rádu na odvodenie invariantov cyklov a súhrnov jednotlivých funkcií analyzovaného programu. Náš prístup je založený na ukazateľových prístupových cestách, ktoré vyjadrujú dosiahnuteľnosť objektov na halde z ukazateľových premenných. Informácie získané z analýzy môžu byť využité na dokázanie rôznych vlastností programu súvisiacich s prácou s dynamickýcmi dátovými štruktúrami. Riešenie bolo implementované v rámci nástroja 2LS. S jeho použitím došlo k výraznému zlepšeniu schopnosti 2LS analyzovať programy pracujúce s ukazateľmi a dynamickými dátovými štruktúrami. Toto je demonštrované na sade experimentov prevzatých zo známej medzinárodnej súťaže vo verifikácii programov SV-COMP a iných experimentoch.