English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Conflict-free replicated data types (CRDTs) are a natural structure withwhich to communicate information about a shared computation in a distributedsetting where coordination overhead may not be tolerated, and individualparticipants are allowed to temporarily diverge from the overall computation.Within this setting, there are two classical approaches: state- andoperation-based CRDTs. The former define a commutative, associative, andidempotent join operation, and their states a monotone join semi-lattice.State-based CRDTs may be further distinguished into classical- and$\delta$-state CRDTs. The former communicate their full state after eachupdate, whereas the latter communicate only the changed state. Op-based CRDTscommunicate operations (not state), thus making their updates non-idempotent.Whereas op-based CRDTs require little information to be exchanged, they demandrelatively strong network guarantees (exactly-once message delivery), andstate-based CRDTs suffer the opposite problem. Both satisfy strong eventualconsistency (SEC).  We posit that $\delta$-state CRDTs both (1) require less communicationoverhead from payload size, and (2) tolerate relatively weak networkenvironments, making them an ideal candidate for real-world use of CRDTs. Ourcentral intuition is a pair of reductions between state-, $\delta$-state, andop-based CRDTs. We formalize this intuition in the Isabelle interactive theoremprover and show that state-based CRDTs achieve SEC. We present a relaxednetwork model in Isabelle and show that state-based CRDTs still maintain SEC.Finally, we extend our work to show that $\delta$-state CRDTs maintain SEC whenonly communicating $\delta$-state fragments, even under relatively weak networkconditions.

Verifying Strong Eventual Consistency in $\delta$-CRDTs