The following is a 2008 conjecture of Abraham, Bonnet and Kubiś: [ABK Conjecture] Every well quasi order (wqo) is a countable union of better quasi orders (bqo). We obtain a partial progress on the conjecture, by showing that the class of orders that are a countable union of better quasi orders (sigma-bqo) is closed under various operations. These include diverse products, such as the Dress-Shieffels product. We develop various properties of the latter product. In relation with the main question, we explore the class of alpha-wqo for countable ordinals alpha and obtain several closure properties and a Hausdorff-style classification theorem. Our main contribution is the discovery of various properties of sigma-bqos and ruling out potential counterexamples to the ABK Conjecture.

The chain covering number $\Cov(P)$ of a poset $P$ is the least number of chains needed to cover $P$. For a cardinal $\nu$, we give a list of posets of cardinality and covering number $\nu$ such that for every poset $P$ with no infinite antichain, $\Cov(P)\geq \nu$ if and only if $P$ embeds a member of the list. This list has two elements if $\nu$ is a successor cardinal, namely $[\nu]^2$ and its dual, and four elements if $\nu$ is a limit cardinal with $\cf(\nu)$ weakly compact. For $\nu= \aleph_1$, a list was given by the first author; his construction was extended by F. Dorais to every infinite successor cardinal $\nu$.

We present a formal framework for proving the correctness of set implementations backed by binary-search-tree (BST) and linked lists, which are often difficult to prove correct using automation. This is because many concurrent set implementations admit non-local linearization points for their `contains' procedure. We demonstrate this framework by applying it to the Contention-Friendly Binary-Search Tree algorithm of Crain et al. We took care to structure our framework in a way that can be easily translated into input for model-checking tools such as TLA+, with the aim of using a computer to verify bounded versions of claims that we later proved manually. Although this approach does not provide complete proof (i.e., does not constitute full verification), it allows checking the reasonableness of the claims before spending effort constructing a complete proof. This is similar to the test-driven development methodology, that has proven very beneficial in the software engineering community. We used this approach and validated many of the invariants and properties of the Contention-Friendly algorithm using TLA+. It proved beneficial, as it helped us avoid spending time trying to prove incorrect claims. In one example, TLA+ flagged a fundamental error in one of our core definitions. We corrected the definition (and the dependant proofs), based on the problematic scenario TLA+ provided as a counter-example. Finally, we provide a complete, manual, proof of the correctness of the Contention-Friendly algorithm, based on the definitions and proofs of our two-tiered framework.

A Tarskian system execution is a structure that describes a run of a system that is composed of several processes. Two types of system executions are defined: temporal based and precedence based. We exemplify the usage of system executions with the specification different types of registers: serial, atomic, safe, and regular.

In his article Teaching Concurrency Lamport stresses the importance of invariants for the education of engineers and computer students, and presents a short algorithm with a challenge to the reader: find an invariant with which a certain simple property of that distributed algorithm can be proved. Our aim is to compare the invariant proof approach to a different one which uses Tarskian system executions rather than invariants. By comparing the details of the two proofs for this simple algorithm we gain a better understanding of these approaches.

The need to handle large programs and to produce efficient compiled code adds complexity to programming languages and limits their expressiveness. Algorithms are not programs, and they can be expressed in a simpler and more expressive language. That language is the one used by almost every branch of science and engineering to precisely describe and reason about the objects they study: the language of mathematics. Math is useful for describing a more general class of algorithms than are studied in algorithm courses.

The aim of this article is to employ the Lazy Set algorithm as an example for a mathematical framework for proving the linearizability of distributed systems. The proof in this approach is divided into two stages of lower and higher abstraction level. At the higher level a list of "axioms" is formulated and a proof is given that any model theoretic structure that satisfies these axioms is linearizable. At this level the algorithm is not mentioned. At the lower level, a Simpler Lazy Set algorithm is described, and it is shown that any execution of this simpler algorithm generates a model of these axioms (and is therefore linearizable). Finally the linearization of the Lazy Set algorithm is obtained by proving that any of its executions has a {\em reduct} that is an execution of the Simpler algorithm. So the reduct executions are linearizable and this entails immediately linearizability of the Lazy Set algorithm itself.

We present an approach for proving the correctness of distributed algorithms that obviate interleaving of processes' actions. The main part of the correctness proof is conducted at a higher abstract level and uses Tarskian system executions that combine two separate issues: the specification of the serial process that executes its protocol alone (no concurrency here), and the specification of the communication objects (no code here). In order to explain this approach a short algorithm for two concurrent processes that we call Kishon's Poker is introduced and is used as a platform where this approach is compared to the standard one which is based on the notions of global state, step, and history.