Masters Degrees (Computer Science)
Permanent URI for this collection
Browse
Browsing Masters Degrees (Computer Science) by browse.metadata.advisor "Inggs, Cornelia P."
Now showing 1 - 4 of 4
Results Per Page
Sort Options
- ItemConcrete and symbolic linearisability checking of non-blocking concurrent data structures(Stellenbosch : Stellenbosch University, 2021-12) Du Toit, Nicole Cathryn; Inggs, Cornelia P.; Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Division Computer Science.ENGLISH ABSTRACT: Non-blocking concurrent data structures are developed as a more efficient solution to concurrent data structures; in non-blocking concurrent data structures hardware-level atomic instructions are used instead of higher-level, expensive locking mechanisms. Lock-free algorithms, however, are notoriously hard to design and prone to subtle concurrency errors that are difficult to pick up. Linearisability Checking is the standard correctness condition for non-blocking concurrent data structures; a data structure is linearisable if each concurrent execution of the data structure corresponds to the execution of its correct sequential specification. In this thesis, the focus is on the linearisability checking of non-blocking data structures using a model checker. The approaches for checking linearisability using a model checker can be broadly categorised into linearisation point and automatic linearisability checking. The state-of-the-art strategies were implemented using the Java PathFinder Model Checker as basis. The linearisation point linearisability checking strategy of Vechev et al. was extended to include data structures with operations that act generically on the data structure, and not just on one element in the data structure. An improved version of Doolan et al.’s external automatic checker was implemented and the idea of an external checker was extended to the improved linearisation point checking strategy. The lazy read optimisation, proposed by Long et al., and a hash optimisation, proposed in this thesis, for the automatic checker was implemented and the effectiveness and benefit of the optimisations determined. The performance-limiting factor of the automatic checker was investigated and the claims made by Vechev et al., Liu et al., and Doolan et al. confirmed/falsified. The concrete checker’s usefulness in finding linearisability errors is constrained by the user’s ability to hand-craft test cases in which errors are present. A new Symbolic Linearisability Checker was developed, the major novel contribution in this thesis, that integrates linearisability checking into Symbolic PathFinder, a symbolic model checker. The symbolic checker performs linearisability checking on all possible test cases and program paths; it verifies the linearisability of a data structure in general, constrained only by a user-defined number of operations to be executed by each thread. Finally, extensive evaluations and comparisons of all checkers were performed, on the same model checking framework and hardware, considering their manual input required, resource usage, scalability, and ability to find errors.
- ItemDetecting and quantifying resource contention in concurrent programs(Stellenbosch : Stellenbosch University, 2016-03) Venter, Dirk Willem; Inggs, Cornelia P.; Stellenbosch University. Faculty of Science. Department of Mathematical Sciences (Computer Science)ENGLISH ABSTRACT : Parallel programs, both shared-memory and message-passing programs, typically require the sharing of resources. For example, software resources, such as shared mutual exclusion locks and hardware resources, such as caches and memory. Shared resources can only be used by one thread or process at a time. The competition for limited resources is called resource contention. The result of resource contention is delays while waiting for access to a resource and/or extra computational overhead to resolve the request for a resource. Thus, the performance of the program can be improved by identifying and reducing contention for shared resources. This study investigates the effect of individual types of contention for hardware and software resources in detail and discusses the three tools that were developed to identify and quantify the sources of contention in concurrent programs.
- ItemLarge language models and software testing(Stellenbosch : Stellenbosch University, 2024-03) Dewey, Marco; Inggs, Cornelia P. ; Visser, Willem; Stellenbosch University. Faculty of Science. Dept. of Computer Science.ENGLISH ABSTRACT: This thesis examines the viability of leveraging transformer-based large language models, exemplified by Codex, f or the a utomated g eneration of test suites in production software. By leveraging the abilities large language models exhibit for understanding and generating natural and coding languages, these models can analyze code and comments to generate contextually relevant test cases. Using these models in the domain of automatic software testing presents a potential solution to the oracle problem. The research involves a comparative analysis between Codex and a promi- nent automatic testing tool, EvoSuite, using the Commons-Lang library from the Defects4J benchmark. This comparison draws insights regarding Codex’s efficacy in ge nerating co verage te sts an d id entifying fa ulty be havior within production code. The findings o f t his thesis a rgue t hat C odex w hile demon- strating promise, exhibits limitations as an automatic testing tool in achieving high test coverage and uncovering software bugs. Moreover, the study high- lights potential challenges associated with utilizing open-source repositories for training and testing code generation by large language models, including the risk of incorporating inconsistent coding conventions and suboptimal software testing practices into these models.
- ItemParallel Monte-Carlo tree search in distributed environments(Stellenbosch : Stellenbosch University., 2020-03) Christoph, Marc; Kroon, R. S. (Steve); Inggs, Cornelia P.; Stellenbosch University. Faculty of Science. Dept. of Mathematical Sciences. Division Computer Science.ENGLISH ABSTRACT: Parallelising Monte-Carlo Tree Search (MCTS) holds the promise of being an effective way to improve the effectiveness of the search, given some time constraint. Thus, finding scalable parallelisation techniques has been an important area of research since MCTS was first proposed. The inherently serial nature of MCTS makes effective parallelisation difficult, since care must be taken to ensure that all threads or processes have access to accurate statistics. This is more challenging in distributed-memory environments due to the latency incurred by network communication.Prior proposals of distributed MCTS have presented their results on different domains and hardware setups, making them difficult to compare.To try to improve this state of affairs, we use the actor-based framework Akka to implement and compare various distributed MCTS algorithms on a common domain—the board game Lines of Action (LOA). We describe our implementation and evaluate the scalability of each approach in terms of play outs per second (PPS), unique nodes searched per second (NPS), and playing strength, STRACTiii. We observe that distributed root parallelisation provides the best PPS scalability, but has relatively poor scalability in terms of NPS. We contrast this with distributed tree parallelisation which scales well in terms of NPS but performs poorly in terms of PPS. Distributed leaf parallelisation is shown to scale up to 128 compute nodes in terms of PPS, but its NPS scalability is limited by its single compute node that manages the tree.We determine that distributed root parallelisation combined with tree parallelisation is the strongest of the distributed MCTS algorithms, with none of our other implementations managing a win-rate of more than 50% against the algorithm. We show that distributed root/leaf parallelisation, as well as our distributed leaf parallelisation with a multi-threaded traverser scale well in terms of playing strength. Distributed tree parallelisation viaTDS, df-UCT and UCT-Treesplit is shown to have limited playing strength scalability, and we provide possible avenues for future work that may resolve this limited performance.We hope that these findings will provide future researchers with sufficient recommendations for implementing distributed MCTS programs.