Truly stateless, optimal dynamic partial order reduction

Dynamic partial order reduction (DPOR) verifies concurrent programs by exploring all their interleavings up to some equivalence relation, such as the Mazurkiewicz trace equivalence. Doing so involves a complex trade-off between space and time. Existing DPOR algorithms are either exploration-optimal (i.e., explore exactly only interleaving per equivalence class) but may use exponential memory in the size of the program, or maintain polynomial memory consumption but potentially explore exponentially many redundant interleavings. In this paper, we show that it is possible to have the best of both worlds: exploring exactly one interleaving per equivalence class with linear memory consumption. Our algorithm, TruSt, formalized in Coq, is applicable not only to sequential consistency, but also to any weak memory model that satisfies a few basic assumptions, including TSO, PSO, and RC11. In addition, TruSt is embarrassingly parallelizable: its different exploration options have no shared state, and can therefore be explored completely in parallel. Consequently, TruSt outperforms the state-of-the-art in terms of memory and/or time.

Program Verification with Separation Logic and Rely Guarantee

<p>This thesis explores two kinds of program logics that have become important for modern program verification - separation logic, for reasoning about programs that use pointers to build mutable data structures, and rely guarantee reasoning, for reasoning about shared variable concurrent programs. We look more closely into the motivations for merging these two kinds of logics into a single formalism that exploits the benefits of both approaches - local, modular, and explicit reasoning about interference between threads in a shared memory concurrent program. We discuss in detail two such formalisms - RGSep and Local Rely Guarantee (LRG), in particular we analyse how each formalism models program state and treats the distinction between global state (shared by all threads) and local state (private to a given thread) and how each logic models actions performed by threads on shared state, and look into the proof rules specifically for reasoning about atomic blocks of code. We present full examples of proofs in each logic and discuss their differences. This thesis also illustrates how a weakest precondition semantics for separation logic can be used to carry out calculational proofs. We also note how in essence these proofs are data abstraction proofs showing that a data structure implements some abstract data type, and relate this idea to a classic data abstraction technique by Hoare. Finally, as part of the thesis we also present a survey of tools that are currently available for doing manual or semi-automated proofs as well as program analyses with separation logic and rely guarantee.</p>

Program Verification with Separation Logic and Rely Guarantee

<p>This thesis explores two kinds of program logics that have become important for modern program verification - separation logic, for reasoning about programs that use pointers to build mutable data structures, and rely guarantee reasoning, for reasoning about shared variable concurrent programs. We look more closely into the motivations for merging these two kinds of logics into a single formalism that exploits the benefits of both approaches - local, modular, and explicit reasoning about interference between threads in a shared memory concurrent program. We discuss in detail two such formalisms - RGSep and Local Rely Guarantee (LRG), in particular we analyse how each formalism models program state and treats the distinction between global state (shared by all threads) and local state (private to a given thread) and how each logic models actions performed by threads on shared state, and look into the proof rules specifically for reasoning about atomic blocks of code. We present full examples of proofs in each logic and discuss their differences. This thesis also illustrates how a weakest precondition semantics for separation logic can be used to carry out calculational proofs. We also note how in essence these proofs are data abstraction proofs showing that a data structure implements some abstract data type, and relate this idea to a classic data abstraction technique by Hoare. Finally, as part of the thesis we also present a survey of tools that are currently available for doing manual or semi-automated proofs as well as program analyses with separation logic and rely guarantee.</p>

Robust self-testing of steerable quantum assemblages and its applications on device-independent quantum certification

Given a Bell inequality, if its maximal quantum violation can be achieved only by a single set of measurements for each party or a single quantum state, up to local unitaries, one refers to such a phenomenon as self-testing. For instance, the maximal quantum violation of the Clauser-Horne-Shimony-Holt inequality certifies that the underlying state contains the two-qubit maximally entangled state and the measurements of one party contains a pair of anti-commuting qubit observables. As a consequence, the other party automatically verifies the set of states remotely steered, namely the "assemblage", is in the eigenstates of a pair of anti-commuting observables. It is natural to ask if the quantum violation of the Bell inequality is not maximally achieved, or if one does not care about self-testing the state or measurements, are we capable of estimating how close the underlying assemblage is to the reference one? In this work, we provide a systematic device-independent estimation by proposing a framework called "robust self-testing of steerable quantum assemblages". In particular, we consider assemblages violating several paradigmatic Bell inequalities and obtain the robust self-testing statement for each scenario. Our result is device-independent (DI), i.e., no assumption is made on the shared state and the measurement devices involved. Our work thus not only paves a way for exploring the connection between the boundary of quantum set of correlations and steerable assemblages, but also provides a useful tool in the areas of DI quantum certification. As two explicit applications, we show 1) that it can be used for an alternative proof of the protocol of DI certification of all entangled two-qubit states proposed by Bowles et al., and 2) that it can be used to verify all non-entanglement-breaking qubit channels with fewer assumptions compared with the work of Rosset et al.

Propositions-as-types and shared state

We develop a principled integration of shared mutable state into a proposition-as-types linear logic interpretation of a session-based concurrent programming language. While the foundation of type systems for the functional core of programming languages often builds on the proposition-as-types correspondence, automatically ensuring strong safety and liveness properties, imperative features have mostly been handled by extra-logical constructions. Our system crucially builds on the integration of nondeterminism and sharing, inspired by logical rules of differential linear logic, and ensures session fidelity, progress, confluence and normalisation, while being able to handle first-class shareable reference cells storing any persistent object. We also show how preservation and, perhaps surprisingly, progress, resiliently survive in a natural extension of our language with first-class locks. We illustrate the expressiveness of our language with examples highlighting detailed features, up to simple shareable concurrent ADTs.

Proof-of-Reputation: An Alternative Consensus Mechanism for Blockchain Systems

Blockchains combine other technologies, such as cryptography, networking, and incentive mechanisms, to enable the creation, validation, and recording of transactions between participating nodes. A consensus algorithm is used in a blockchain system to determine the shared state among distributed nodes. An important component underlying any blockchain-based system is its consensus mechanism, which principally determines the performance and security of the overall system. As the nature of peer-topeer(P2P) networks is open and dynamic, the security risk within that environment is greatly increased mostly because nodes can join and leave the network at will. Thus, it is important to have a system that can check against malicious behaviour. In this work, we propose a reputation-based consensus mechanism for blockchain-based systems, Proof-of-Reputation(PoR) where the nodes with the highest reputation values eventually become part of a consensus group that determines the state of the blockchain.

Studying the Applicability of Proof of Reputation(PoR) as an Alternative Consensus Mechanism for Distributed Ledger Systems

Blockchains combine several other technologies like cryptography, networking, and incentive mechanisms in order to support the creation, validation, and recording of transactions between participating nodes. A blockchain system relies on a consensus algorithm to determine the shared state among distributed nodes. An important component underlying any blockchainbased system is its consensus mechanism, which determines the characteristics of the overall system. This thesis proposes a reputation-based consensus mechanism for blockchain-based systems which we term Proof-of-Reputation(PoR) that uses the liquid rank algorithm where the reputation of a node is calculated by blending the normalized ratings by other nodes in the network for a given period with the reputation values of the nodes giving the ratings. The nodes with the highest reputation values eventually become part of the consensus group that determines the state of the blockchain.

Ghost Signals: Verifying Termination of Busy Waiting

Programs for multiprocessor machines commonly perform busy waiting for synchronization. We propose the first separation logic for modularly verifying termination of such programs under fair scheduling. Our logic requires the proof author to associate a ghost signal with each busy-waiting loop and allows such loops to iterate while their corresponding signal $$s$$ s is not set. The proof author further has to define a well-founded order on signals and to prove that if the looping thread holds an obligation to set a signal $$s'$$ s ′ , then $$s'$$ s ′ is ordered above $$s$$ s . By using conventional shared state invariants to associate the state of ghost signals with the state of data structures, programs busy-waiting for arbitrary conditions over arbitrary data structures can be verified.