Refine
Year of publication
Document Type
- In Proceedings (43)
- Article (30)
- ZIB-Report (6)
- Other (4)
- Book chapter (3)
- Poster (2)
- Doctoral Thesis (1)
- Master's Thesis (1)
Is part of the Bibliography
- no (90) (remove)
Keywords
- DHT (2)
- Cache-Simulator (1)
- Grid computing (1)
- Kostenmodell (1)
- Microbenchmarks (1)
- P2P (1)
- Paxos (1)
- Range Queries (1)
- SMP-System (1)
- Speicherhierarchie (1)
General solutions of state machine replication have to ensure that all replicas apply the same commands in the same order, even in the presence of failures. Such strict ordering incurs high synchronization costs due to the use of distributed consensus or a leader.
This paper presents a protocol for linearizable state machine replication of conflict-free replicated data types (CRDTs) that neither requires consensus nor a leader. By leveraging the properties of state-based CRDTs—in particular the monotonic growth of a join semilattice—synchronization overhead is greatly reduced. In addition, updates just need a single round trip and modify the state ‘in-place’ without the need for a log. Furthermore, the message size overhead for coordination consists of a single counter per message. While reads in the presence of concurrent updates are not wait-free without a coordinator, we show that more than 97 % of reads can be handled in one or two round trips under highly concurrent accesses.
Our protocol achieves high throughput without auxiliary processes such as command log management or leader election. It is well suited for all practical scenarios that need linearizable access on CRDT data on a fine-granular scale.
Learned clauses minimization (LCM) let to performance improvements of modern SAT solvers especially in solving hard SAT instances. Despite the success of LCM approaches in sequential solvers, they are not widely incorporated in parallel SAT solvers. In this paper we explore the potential of LCM for parallel SAT solvers by defining multiple LCM approaches based on clause vivification, comparing their runtime in different SAT solvers and discussing reasons for performance gains and losses. Results show that LCM only boosts performance of parallel SAT solvers on a fraction of SAT instances. More commonly applying LCM decreases performance. Only certain LCM approaches are able to improve the overall performance of parallel SAT solvers.