M.Sc. (Computer Science) / Please refer to full text to view abstract

As services grow and receive more traffic, data resilience through replication becomes increasingly important. Modern large-scale Internet services such as Facebook, Google and Twitter serve millions of users concurrently. Replication is a vital component of distributed systems. Eventual consistency and Conflict-Free Replicated Data Types (CRDTs) are suggested as an alternative to strong consistency systems. This thesis implements and evaluates Snapple, a distributed, fault-tolerant, in-memory key-value database based on CRDTs running on the Java Virtual Machine. Snapple supports two kinds of CRDTs, an optimized implementation of the OR-Set and version vectors. Performance measurements show that the Snapple system is significantly faster than Riak, a persistent database based on CRDTs, but has a factor 5x - 2.5x lower throughput than Redis, a popular in-memory key-value database written in C. Snapple is a prototype-implementation but might be a viable alternative to Redis if the user wants the consistency guarantees CRDTs provide. / När internet-baserade tjänster växer och får mer trafik blir data replikering allt viktigare. Moderna storskaliga internet-baserade tjänster såsom Facebook, Google och Twitter hanterar miljoner av förfrågningar från användare samtidigt. Datareplikering är en vital komponent av distribuerade system. Eventuell synkronisering och Konfliktfria Replikerade Datatyper (CRDTs) är föreslagna som alternativ till direkt synkronisering. Denna uppsats implementerar och evaluerar Snapple, en distribuerad feltolerant nyckelvärdesdatabas i RAM-minnet baserad på CRDTs och som exekverar på Javas virtuella maskin. Snapple stödjer två sorters CRDTs, den optimerade implementationen av observera-ta-bort setet och versionsvektorer. Prestanda-mätningar visar att Snapple-systemet är mycket snabbare än Riak, en persistent databas baserad på CRDTs. Snapple visar sig ha 5x - 2.5x lägre genomströmning än Redis, en popular i-minnet nyckel-värdes databas skriven i C. Snapple är en prototyp men CRDT-stödda system kan vara ett värdigt alternativ till Redis om användaren vill ta del av synkroniseringsgarantierna som CRDTs tillhandahåller.

Background: Computers use sorting algorithms to prepare data for search or insert operations, these operations can be a bottleneck for performance. Objectives: To evaluate sorting algorithms performances when existing in different implementation environments like different languages, sorting in different data types and in different sizes. Methods: By performing an experiment with Java, C++, Python and Javascript on three different sizes and three different data types performance of sorting algorithms will be evaluated. The sorting algorithms used in this study are Insertion sort, Selection sort, Quick sort and Merge sort. They were all tested on each size on each language three times. Results: In the end 432 tests were performed and the results found that Java had best execution time on all four algorithms with quick sort as the best algorithm. The best data type could not be pinpointed down since they acted differently on different algorithms. Quicksort was determined to be the fastest algorithm in the literature review which focused fastest algorithm Conclusions: Together with the results of the experiment and literature review quicksort is the fastest sorting algorithm. The best performing implementation language was Java. For data types one type could not be determined the best only the worse could be decided, floats performed the worse of all three types.

Generalized algebraic data types (GADTs) are a type system extension to algebraic data types that allows the type of an algebraic data value to vary with its shape. The GADT type system allows programmers to express detailed program properties as types (for example, that a function should return a list of the same length as its input), and a general-purpose type checker will automatically check those properties at compile time. Type inference for the GADT type system and the properties of the type system are both currently areas of active research. In this dissertation, I attack both problems simultaneously by exploiting the symbiosis between type system research and type inference research. Deficiencies of GADT type inference algorithms motivate research on specific aspects of the type system, and discoveries about the type system bring in new insights that lead to improved GADT type inference algorithms. The technical contributions of this dissertation are therefore twofold: in addition to new GADT type system properties (such as the prevalence of pointwise type information flow in GADT patterns, a generalized notion of existential types, and the effects of enforcing the GADT branch reachability requirement), I will also present a new GADT type inference algorithm that is significantly more powerful than existing algorithms. These contributions should help programmers use the GADT type system more effectively, and they should also enable language implementers to provide better support for the GADT type system.

Mobile applications often must synchronize their local state with a backend to maintain an up-to-date view of the application state. Nevertheless, in some cases, the application’s ability to work offline or with poor network connectivity may be more significant than guaranteeing strong consistency. We present a method to structure the application state in a portable way using the Redux pattern and the properties of strongly typed languages. This method allows employing Conflict-free Replicated Data Types to create a custom converging state: this way, each replica can edit its local state autonomously and merge conflicts with other replicas when possible. Furthermore, we propose to keep a server as the communication channel and analyze how this architecture impacts design choices and optimizations related to CRDTs. Finally, we evaluate our method on a note-taking application using a few well-known CRDT designs and quantitatively justify our design choices. / Mobilapplikationer måste ofta synkronisera lokala tillstånd med backend för att upprätthålla en uppdaterad vy av applikationstillstånd. I vissa fall kan dock applikationens förmåga att arbeta offline eller med dålig nätverksanslutning vara viktigare än att garantera strong consistency. Vi presenterar en metod för att strukturera applikationstillståndet på ett portabelt sätt med hjälp av Redux-mönstret och egenskaperna hos starkt typade språk. Den här metoden gör det möjligt att använda Conflict-free Replicated Data Types för att skapa ett anpassat konvergerande tillstånd: på så sätt kan varje replik redigera sin lokala status självständigt och slå samman konflikter med andra repliker när det är möjligt. Dessutom föreslår vi att behålla en server som kommunikationskanal och analysera hur denna arkitektur påverkar designval och optimeringar relaterade till CRDT. Slutligen utvärderar vi vår metod på en anteckningsapplikation med några välkända CRDT-designer och motiverar kvantitativt våra designval. / Le applicazioni mobile spesso devono sincronizzare il loro stato locale con il back-end per mantenere una visione aggiornata dello stato dell’applicazione. Tuttavia, in alcuni casi, la capacità dell’applicazione di funzionare offline o con una scarsa connettività può essere più importante del garantire la “strong consistency”. In questa tesi presentiamo un metodo per strutturare lo stato di un’applicazione in modo portabile utilizzando il pattern Redux e le proprietà dei linguaggi fortemente tipizzati. Questo metodo consente di utilizzare i Conflict-free Replicated Data Types per creare uno stato convergente ad hoc: in questo modo, ogni replica può modificare il proprio stato locale in modo autonomo e risolvere i conflitti con le altre repliche quando possibile. Inoltre, proponiamo di mantenere un server come canale di comunicazione e di analizzare come questa architettura influisca sulle scelte progettuali e sulle ottimizzazioni relative ai CRDT. Infine, valutiamo il nostro metodo su un’applicazione per prendere appunti utilizzando alcuni CRDT noti e giustifichiamo quantitativamente le nostre scelte di progettazione.

The exponential increase in online text has created a pressing need for automatic summarization systems that can distill key information from lengthy documents. While neural abstractive summarizers have achieved gains in fluency and coherence, a critical challenge that has emerged is ensuring faithfulness, i.e., accurately preserving the meaning from the original text. Modern neural abstractive summarizers can distort or fabricate facts, undermining their reliability in real-world applications. Thus, this thesis tackles the critical issue of improving faithfulness in abstractive summarization. This thesis is comprised of four parts. The first part examines challenges in evaluating summarization faithfulness, including issues with reference-free metrics and human evaluation. We propose a novel approach for building automated evaluation metrics that are less reliant on spurious correlations and demonstrate significantly improved performance over existing faithfulness evaluation metrics. We further introduce a novel evaluation framework that enables a more holistic assessment of faithfulness by accounting for the abstractiveness of summarization systems. This framework enables more rigorous faithfulness evaluation, differentiating between gains from increased extraction versus improved abstraction. The second part focuses on explaining the root causes of faithfulness issues in modern summarization systems. We introduce a novel contrastive approach for attributing errors that vastlyoutperforms prior work at tracing hallucinations in generated summaries back to training data deficiencies. Moreover, incorporating our method’s ideas into an existing technique substantially boosts its performance. Through a case study, we also analyze pre-training biases and demonstrate their propagation to summarization models, yielding biased hallucinations. We show that while mitigation strategies during finetuning can reduce overall hallucination rates, the remaining hallucinations still closely reflect intrinsic pre-training biases. The third part applies insights from previous sections to develop impactful techniques for improving faithfulness in practice. We propose a novel approach for adaptively determining the appropriate level of abstractiveness for a given input to improve overall faithfulness. Our method yields systems that are both more faithful and more abstractive compared to baseline systems. We further leverage our error attribution approach to clean noisy training data, significantly reducing faithfulness errors in generated outputs. Models trained on datasets cleaned with our approach generate markedly fewer hallucinations than both baseline systems and models trained using other data cleaning techniques. Finally, the fourth part examines the summarization capabilities of LLMs and assesses their faithfulness. We demonstrate that instruction-tuning and RLHF are key for enabling LLMs to achieve high-quality zero-shot summarization in the news domain, with state-of-the-art LLMs generating summaries comparable to human-written ones. However, this ability does not extend to narrative summarization, where even advanced LLMs struggle to produce consistently faithful summaries. Finally, we highlight the difficulty in evaluating high-performing LLMs, showing that crowdsourcing evaluations of LLM outputs may no longer be reliable as fluency and coherence improve. We observe a substantial gap between crowd workers and experts in identifying deficiencies in LLM-generated narrative summaries.

No / Medical statistics is a vast and ever-growing field of academic endeavour, with direct application to developing the robustness of the evidence base in all areas of medicine. Although the complexity of available statistical techniques has continued to increase, fuelled by the rapid data processing capabilities of even desktop/laptop computers, medical practitioners can go a long way towards creating, critically evaluating and assimilating this evidence with an understanding of just a few key statistical concepts. While the concepts of statistics and ethics are not common bedfellows, it should be emphasised that a statistically flawed study is also an unethical study.[1] This review will outline some of these key concepts and explain how to interpret the output of some commonly used statistical analyses. Examples will be confined to two-group tests on independent samples, using both a continuous and a dichotomous/binary outcome measure.

Práce se zaobírá problematikou implementace součtového datového typu v jazyce C++. Nejprve navrhuje vlastní abstrakce pro manipulaci s posloupnostmi hodnot a typů, které následně umožňují vyjadřovat komplexní operace deklarativně. V průběhu implementace jsou prezentovány návrhové vzory obvyklé pro oblast metaprogramování. Implementace přichází s rozhodnutími odlišnými od referenční implementace. Pro manipulaci se součtovým typem jsou představeny dvě šablony funkce, lišící se sémantikou. Užití součtového typu je ukázano na příkladu konečného stavového automatu.

by Keith, Hang-kwong Mak. / Thesis (M.Phil.)--Chinese University of Hong Kong, 1995. / Includes bibliographical references (leaves 122-127). / Abstract --- p.i / Acknowledgement --- p.iii / Chapter 1 --- Introduction --- p.1 / Chapter 2 --- Background --- p.4 / Chapter 2.1 --- Read/Write Model --- p.4 / Chapter 2.2 --- Abstract Data Type Model --- p.5 / Chapter 2.3 --- Overview of Semantics-Based Concurrency Control Protocols --- p.7 / Chapter 2.4 --- Concurrency Hierarchy --- p.9 / Chapter 2.5 --- Control Flow of the Strict Two Phase Locking Protocol --- p.11 / Chapter 2.5.1 --- Flow of an Operation --- p.12 / Chapter 2.5.2 --- Response Time of a Transaction --- p.13 / Chapter 2.5.3 --- Factors Affecting the Response Time of a Transaction --- p.14 / Chapter 3 --- Semantics-Based Concurrency Control Protocols --- p.16 / Chapter 3.1 --- Strict Two Phase Locking --- p.16 / Chapter 3.2 --- Conflict Relations --- p.17 / Chapter 3.2.1 --- Commutativity (COMM) --- p.17 / Chapter 3.2.2 --- Forward and Right Backward Commutativity --- p.19 / Chapter 3.2.3 --- Exploiting Context-Specific Information --- p.21 / Chapter 3.2.4 --- Relaxing Correctness Criterion by Allowing Bounded Inconsistency --- p.26 / Chapter 4 --- Related Work --- p.32 / Chapter 4.1 --- Exploiting Transaction Semantics --- p.32 / Chapter 4.2 --- Exploting Object Semantics --- p.34 / Chapter 4.3 --- Sacrificing Consistency --- p.35 / Chapter 4.4 --- Other Approaches --- p.37 / Chapter 5 --- Performance Study (Testbed Approach) --- p.39 / Chapter 5.1 --- System Model --- p.39 / Chapter 5.1.1 --- Main Memory Database --- p.39 / Chapter 5.1.2 --- System Configuration --- p.40 / Chapter 5.1.3 --- Execution of Operations --- p.41 / Chapter 5.1.4 --- Recovery --- p.42 / Chapter 5.2 --- Parameter Settings and Performance Metrics --- p.43 / Chapter 6 --- Performance Results and Analysis (Testbed Approach) --- p.46 / Chapter 6.1 --- Read/Write Model vs. Abstract Data Type Model --- p.46 / Chapter 6.2 --- Using Context-Specific Information --- p.52 / Chapter 6.3 --- Role of Conflict Ratio --- p.55 / Chapter 6.4 --- Relaxing the Correctness Criterion --- p.58 / Chapter 6.4.1 --- Overhead and Performance Gain --- p.58 / Chapter 6.4.2 --- Range Queries using Bounded Inconsistency --- p.63 / Chapter 7 --- Performance Study (Simulation Approach) --- p.69 / Chapter 7.1 --- Simulation Model --- p.70 / Chapter 7.1.1 --- Logical Queueing Model --- p.70 / Chapter 7.1.2 --- Physical Queueing Model --- p.71 / Chapter 7.2 --- Experiment Information --- p.74 / Chapter 7.2.1 --- Parameter Settings --- p.74 / Chapter 7.2.2 --- Performance Metrics --- p.75 / Chapter 8 --- Performance Results and Analysis (Simulation Approach) --- p.76 / Chapter 8.1 --- Relaxing Correctness Criterion of Serial Executions --- p.77 / Chapter 8.1.1 --- Impact of Resource Contention --- p.77 / Chapter 8.1.2 --- Impact of Infinite Resources --- p.80 / Chapter 8.1.3 --- Impact of Limited Resources --- p.87 / Chapter 8.1.4 --- Impact of Multiple Resources --- p.89 / Chapter 8.1.5 --- Impact of Transaction Type --- p.95 / Chapter 8.1.6 --- Impact of Concurrency Control Overhead --- p.96 / Chapter 8.2 --- Exploiting Context-Specific Information --- p.98 / Chapter 8.2.1 --- Impact of Limited Resource --- p.98 / Chapter 8.2.2 --- Impact of Infinite and Multiple Resources --- p.101 / Chapter 8.2.3 --- Impact of Transaction Length --- p.106 / Chapter 8.2.4 --- Impact of Buffer Size --- p.108 / Chapter 8.2.5 --- Impact of Concurrency Control Overhead --- p.110 / Chapter 8.3 --- Summary and Discussion --- p.113 / Chapter 8.3.1 --- Summary of Results --- p.113 / Chapter 8.3.2 --- Relaxing Correctness Criterion vs. Exploiting Context-Specific In- formation --- p.114 / Chapter 9 --- Conclusions --- p.116 / Bibliography --- p.122 / Chapter A --- Commutativity Tables for Queue Objects --- p.128 / Chapter B --- Specification of a Queue Object --- p.129 / Chapter C --- Commutativity Tables with Bounded Inconsistency for Queue Objects --- p.132 / Chapter D --- Some Implementation Issues --- p.134 / Chapter D.1 --- Important Data Structures --- p.134 / Chapter D.2 --- Conflict Checking --- p.136 / Chapter D.3 --- Deadlock Detection --- p.137 / Chapter E --- Simulation Results --- p.139 / Chapter E.l --- Impact of Infinite Resources (Bounded Inconsistency) --- p.140 / Chapter E.2 --- Impact of Multiple Resource (Bounded Inconsistency) --- p.141 / Chapter E.3 --- Impact of Transaction Type (Bounded Inconsistency) --- p.142 / Chapter E.4 --- Impact of Concurrency Control Overhead (Bounded Inconsistency) --- p.144 / Chapter E.4.1 --- Infinite Resources --- p.144 / Chapter E.4.2 --- Limited Resource --- p.146 / Chapter E.5 --- Impact of Resource Levels (Exploiting Context-Specific Information) --- p.149 / Chapter E.6 --- Impact of Buffer Size (Exploiting Context-Specific Information) --- p.150 / Chapter E.7 --- Impact of Concurrency Control Overhead (Exploiting Context-Specific In- formation) --- p.155 / Chapter E.7.1 --- Impact of Infinite Resources --- p.155 / Chapter E.7.2 --- Impact of Limited Resources --- p.157 / Chapter E.7.3 --- Impact of Transaction Length --- p.160 / Chapter E.7.4 --- Role of Conflict Ratio --- p.162

Any analysis of higher-order languages must grapple with the tri-facetted nature of lambda. In one construct, the fundamental control, environment and data structures of a language meet and intertwine. With the control facet tamed nearly two decades ago, this work brings the environment facet to heel, defining the environment problem and developing its solution: environment analysis. Environment analysis allows a compiler to reason about the equivalence of environments, i.e., name-to-value mappings, that arise during a program's execution. In this dissertation, two different techniques-abstract counting and abstract frame strings-make this possible. A third technique, abstract garbage collection, makes both of these techniques more precise and, counter to intuition, often faster as well. An array of optimizations and even deeper analyses which depend upon environment analysis provide motivation for this work. In an abstract interpretation, a single abstract entity represents a set of concrete entities. When the entities under scrutiny are bindings-single name-to-value mappings, the atoms of environment-then determining when the equality of two abstract bindings infers the equality of their concrete counterparts is the crux of environment analysis. Abstract counting does this by tracking the size of represented sets, looking for singletons, in order to apply the following principle: If {x} = {y}, then x = y. Abstract frame strings enable environmental reasoning by statically tracking the possible stack change between the births of two environments; when this change is effectively empty, the environments are equivalent. Abstract garbage collection improves precision by intermittently removing unreachable environment structure during abstract interpretation.