Typical models of resource-sharing real-time tasks provide the worst-case task execution time and the duration of each critical section during which a resource is accessed. Such models abstract away the detailed behavior of a task, which may make several individual accesses within a single critical section, incurring access overhead once for the entire critical section. Considering a more fine-grained model with individual access and non-access segments at the forefront gives more control in the system design process; choosing how accesses are grouped into critical sections enables balancing trade-offs between overhead and blocking based on other system parameters, including task deadlines. This paper presents an optimal approach for multi-resource systems that allow any given task to use up to two resources, including support for nested critical sections. This is achieved by extending analysis to multiple resources and constructing a Quadratically-Constrained Integer Program to determine critical sections. This approach is compared to heuristics on the basis of schedulability and its runtime is explored. Further extension to support more resources per task is discussed.

First-generation blockchains provide probabilistic finality: a block can be revoked, albeit the probability decreases as the block "sinks" deeper into the chain. Recent proposals revisited committee-based BFT consensus to provide deterministic finality: as soon as a block is validated, it is never revoked. A distinguishing characteristic of these second-generation blockchains over classical BFT protocols is that committees change over time as the participation and the blockchain state evolve. In this paper, we push forward in this direction by proposing a formalization of the Dynamic Repeated Consensus problem and by providing generic procedures to solve it in the context of blockchains. Our approach is modular in that one can plug in different synchronizers and single-shot consensus. To offer a complete solution, we provide a concrete instantiation, called {{Tenderbake}}, and present a blockchain synchronizer and a single-shot consensus algorithm, working in a Byzantine and partially synchronous system model with eventually synchronous clocks. In contrast to recent proposals, our methodology is driven by the need to bound the message buffers. This is essential in preventing spamming and run-time memory errors. Moreover, {{Tenderbake}} processes can synchronize with each other without exchanging messages, leveraging instead the information stored in the blockchain.

Preference aggregation is a fundamental problem in voting theory, in which public input rankings of a set of alternatives (called preferences) must be aggregated into a single preference that satisfies certain soundness properties. The celebrated Arrow Impossibility Theorem is equivalent to a distributed task in a synchronous fault-free system that satisfies properties such as respecting unanimous preferences, maintaining independence of irrelevant alternatives (IIA), and non-dictatorship, along with consensus since only one preference can be decided. In this work, we study a weaker distributed task in which crash faults are introduced, IIA is not required, and the consensus property is relaxed to either k-set agreement or ε-approximate agreement using any metric on the set of preferences. In particular, we prove several novel impossibility results for both of these tasks in both synchronous and asynchronous distributed systems. We additionally show that the impossibility for our ε-approximate agreement task using the Kendall tau or Spearman footrule metrics holds under extremely weak assumptions.

Graph pebbling is a combinatorial game played on an undirected graph with an initial configuration of pebbles. A pebbling move consists of removing two pebbles from one vertex and placing one pebble on an adjacent vertex. The pebbling number of a graph is the smallest number of pebbles necessary such that, given any initial configuration of pebbles, at least one pebble can be moved to a specified root vertex. Recent lines of inquiry apply computational techniques to pebbling bound generation and improvement. Along these lines, we present a computational framework that produces a set of tree strategy weight functions that are capable of proving pebbling number upper bounds on a connected graph. Our mixed-integer linear programming approach automates the generation of large sets of such functions and provides verifiable certificates of pebbling number upper bounds. The framework is capable of producing verifiable pebbling bounds on any connected graph, regardless of its structure or pebbling properties. We apply the model to the 4th weak Bruhat to prove π ( B 4 ) ≤ 66 and to the Lemke square graph to produce a set of certificates that verify π ( L □ L ) ≤ 96 .

We describe a general and safe computational framework that provides integer programming results with the degree of certainty that is required for machine-assisted proofs of mathematical theorems. At its core, the framework relies on a rational branch-and-bound certificate produced by an exact integer programming solver, SCIP, in order to circumvent floating-point round-off errors present in most state-of-the-art solvers for mixed-integer programs. The resulting certificates are self-contained and checker software exists that can verify their correctness independently of the integer programming solver used to produce the certificate. This acts as a safeguard against programming errors that may be present in complex solver software. The viability of this approach is tested by applying it to finite cases of Chvátal’s conjecture, a long-standing open question in extremal combinatorics. We take particular care to verify also the correctness of the input for this specific problem, using the Coq formal proof assistant. As a result, we are able to provide the first machine-assisted proof that Chvátal’s conjecture holds for all downsets whose union of sets contains seven elements or less.

High-performance simulations and parallel frameworks often rely on highly scalable, concurrent data structures for system scalability. With an increased availability of NUMA architectures, we present a technique to promote NUMA-aware data parallelism inside a concurrent data structure, bringing significant quantitative and qualitative improvements on NUMA locality, as well as reduced contention for synchronized memory accesses. Our architecture is based on a data-partitioned, concurrent skip graph indexed by thread-local sequential maps. We implemented maps and relaxed priority queues using such technique. Maps show up to 6x higher CAS locality, up to a 68.6% reduction on the number of remote CAS operations, and an increase from 88.3% to 99% on the CAS success rate compared to a control implementation (subject to the same optimizations, and implementation practices). Remote memory accesses are not only reduced in number, but the larger the NUMA distance between threads, the larger the reduction is. Relaxed priority queues implemented using our technique show similar scalability improvements, with provable reduction in contention and decrease in relaxation in one of our implementations.