arXiv subjects

Suha Orhun Mutluergil

Publications and source records attributed to Suha Orhun Mutluergil.

7 recordsLinked to original sources

arXiv2026

Combining Axiomatic Models for Refinement Proofs

Refinement proofs verify an implementation by showing that its behaviours are subsumed by a simpler specification, on which safety properties are easier to establish. We study how such proofs interact with the axiomatic program logics used to verify the specification. We first give a uniform account of Hoare, Incorrectness, Lisbon, and Necessary-Preconditions logic, classified by the direction in which each constrains a transition and by whether it over- or under-approximates its target set. We then show that simulation relations transfer state-based safety properties: a forward simulation carries a Hoare (inductive) invariant of the specification to one of the implementations, and forward and backward simulations both carry ordinary invariants, via the pre-image of the relation. Finally, we characterize, within these logics, when a relation is a simulation, forward simulations by the validity of Hoare or Lisbon triples, backward simulations by Necessary-Preconditions or Incorrectness triples, so that the simulation obligation reduces to a triple in an off-the-shelf functional logic. We illustrate the development with a concurrent counter, transporting a safety bound from an atomic sequential specification to a Left--Right implementation through an intermediate nondeterministic-concurrent counter, with a forward simulation on one side and a backward simulation on the other.

cs.LO↗

arXiv2024

Going Forward-Forward in Distributed Deep Learning

We introduce a new approach in distributed deep learning, utilizing Geoffrey Hinton's Forward-Forward (FF) algorithm to speed up the training of neural networks in distributed computing environments. Unlike traditional methods that rely on forward and backward passes, the FF algorithm employs a dual forward pass strategy, significantly diverging from the conventional backpropagation process. This novel method aligns more closely with the human brain's processing mechanisms, potentially offering a more efficient and biologically plausible approach to neural network training. Our research explores different implementations of the FF algorithm in distributed settings, to explore its capacity for parallelization. While the original FF algorithm focused on its ability to match the performance of the backpropagation algorithm, the parallelism aims to reduce training times and resource consumption, thereby addressing the long training times associated with the training of deep neural networks. Our evaluation shows a 3.75 times speed up on MNIST dataset without compromising accuracy when training a four-layer network with four compute nodes. The integration of the FF algorithm into distributed deep learning represents a significant step forward in the field, potentially revolutionizing the way neural networks are trained in distributed environments.

cs.LG↗

arXiv2023

Quorum Tree Abstractions of Consensus Protocols

Distributed algorithms solving agreement problems like consensus or state machine replication are essential components of modern fault-tolerant distributed services. They are also notoriously hard to understand and reason about. Their complexity stems from the different assumptions on the environment they operate with, i.e., process or network link failures, Byzantine failures etc. In this paper, we propose a novel abstract representation of the dynamics of such protocols which focuses on quorums of responses (votes) to a request (proposal) that form during a run of the protocol. We show that focusing on such quorums, a run of a protocol can be viewed as working over a tree structure where different branches represent different possible outcomes of the protocol, the goal being to stabilize on the choice of a fixed branch. This abstraction resembles the description of recent protocols used in Blockchain infrastructures, e.g., the protocol supporting Bitcoin or HotStuff. We show that this abstraction supports reasoning about the safety of various algorithms, e.g., Paxos, PBFT, Raft, and HotStuff, in a uniform way. In general, it provides a novel induction based argument for proving that such protocols are safe.

cs.DC↗

arXiv2022

A Pragmatic Approach to Stateful Partial Order Reduction

Partial order reduction (POR) is a classic technique for dealing with the state explosion problem in model checking of concurrent programs. Theoretical optimality, i.e., avoiding enumerating equivalent interleavings, does not necessarily guarantee optimal overall performance of the model checking algorithm. The computational overhead required to guarantee optimality may by far cancel out any benefits that an algorithm may have from exploring a smaller state space of interleavings. With a focus on overall performance, we propose new algorithms for stateful POR based on the recently proposed source sets, which are less precise but more efficient than the state of the art in practice. We evaluate efficiency using an implementation that extends Java Pathfinder in the context of verifying concurrent data structures.

cs.DC↗

arXiv2019

Replication-Aware Linearizability

Geo-distributed systems often replicate data at multiple locations to achieve availability and performance despite network partitions. These systems must accept updates at any replica and propagate these updates asynchronously to every other replica. Conflict-Free Replicated Data Types (CRDTs) provide a principled approach to the problem of ensuring that replicas are eventually consistent despite the asynchronous delivery of updates. We address the problem of specifying and verifying CRDTs, introducing a new correctness criterion called Replication-Aware Linearizability. This criterion is inspired by linearizability, the de-facto correctness criterion for (shared-memory) concurrent data structures. We argue that this criterion is both simple to understand, and it fits most known implementations of CRDTs. We provide a proof methodology to show that a CRDT satisfies replication-aware linearizability which we apply on a wide range of implementations. Finally, we show that our criterion can be leveraged to reason modularly about the composition of CRDTs.

cs.PL↗

arXiv2018

Reasoning About TSO Programs Using Reduction and Abstraction

We present a method for proving that a program running under the Total Store Ordering (TSO) memory model is robust, i.e., all its TSO computations are equivalent to computations under the Sequential Consistency (SC) semantics. This method is inspired by Lipton's reduction theory for proving atomicity of concurrent programs. For programs which are not robust, we introduce an abstraction mechanism that allows to construct robust programs over-approximating their TSO semantics. This enables the use of proof methods designed for the SC semantics in proving invariants that hold on the TSO semantics of a non-robust program. These techniques have been evaluated on a large set of benchmarks using the infrastructure provided by CIVL, a generic tool for reasoning about concurrent programs under the SC semantics.

cs.LO↗

arXiv2017

Proving linearizability using forward simulations

Linearizability is the standard correctness criterion concurrent data structures such as stacks and queues. It allows to establish observational refinement between a concurrent implementation and an atomic reference implementation.Proving linearizability requires identifying linearization points for each method invocation along all possible computations, leading to valid sequential executions, or alternatively, establishing forward and backward simulations. In both cases, carrying out proofs is hard and complex in general. In particular, backward reasoning is difficult in the context of programs with data structures, and strategies for identifying statically linearization points cannot be defined for all existing implementations. In this paper, we show that, contrary to common belief, many such complex implementations, including, e.g., the Herlihy&Wing Queue and the Time-Stamped Stack, can be proved correct using only forward simulation arguments. This leads to conceptually simple and natural correctness proofs for these implementations that are amenable to automation.

cs.PL↗