skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Merge what you can, fork what you can't: managing data integrity in local-first software
In a local-first architecture that prioritizes availability in the presence of network partitions, there is a tension between two goals: merging concurrent changes without user intervention and maintaining data integrity constraints. We propose a synchronization model called forking histories which satisfies both goals in an unconventional way. In the case of conflicting writes, the model exposes multiple event histories that users can see and edit rather than converging to a single state. This allows integrity constraints to be maintained within each history while giving users flexibility in deciding when to manually reconcile conflicts. We describe a class of applications for which these integrity constraints are particularly important and propose a design for a system that implements this model.  more » « less
Award ID(s):
1801399
PAR ID:
10353997
Author(s) / Creator(s):
; ;
Date Published:
Journal Name:
Proceedings of the 9th Workshop on Principles and Practice of Consistency for Distributed Data
Page Range / eLocation ID:
24 to 32
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. In recent years, a range of online applications have facilitated resource sharing among users, resulting in a significant increase in resource utilization. In all such applications, sharing one’s resources or skills with other agents increases social welfare. In general, each agent will look for other agents whose available resources complement hers, thereby forming natural sharing groups. In this paper, we study settings where a large population self-organizes into sharing groups. In many cases, centralized optimization approaches for creating an optimal partition of the user population are infeasible because either the central authority does not have the necessary information to compute an optimal partition, or it does not have the power to enforce a partition. Instead, the central authority puts in place an incentive structure in the form of a utility sharing method, before letting the participants form the sharing groups by themselves. We first analyze a simple equal-sharing method, which is the one most typically encountered in practice and show that it can lead to highly inefficient equilibria. We then propose a Shapley-sharing method and show that it significantly improves overall social welfare. 
    more » « less
  2. null (Ed.)
    In this paper, we consider a temporal logic planning problem in which the objective is to find an infinite trajectory that satisfies an optimal selection from a set of soft specifications expressed in linear temporal logic (LTL) while nevertheless satisfying a hard specification expressed in LTL. Our previous work considered a similar problem in which linear dynamic logic for finite traces (LDL_f), rather than LTL, was used to express the soft constraints. In that work, LDL_f was used to impose constraints on finite prefixes of the infinite trajectory. By using LTL, one is able not only to impose constraints on the finite prefixes of the trajectory, but also to set `soft' goals across the entirety of the infinite trajectory. Our algorithm first constructs a product automaton, on which the planning problem is reduced to computing a lasso with minimum cost. Among all such lassos, it is desirable to compute a shortest one. Though we prove that computing such a shortest lasso is computationally hard, we also introduce an efficient greedy approach to synthesize short lassos nonetheless. We present two case studies describing an implementation of this approach, and report results of our experiment comparing our greedy algorithm with an optimal baseline. 
    more » « less
  3. Traditional Internet routing is simple, scalable and robust, but cannot provide perfect QoS support due to the current completely distributed hop-by-hop routing architecture. Software defined networking (SDN) opens up the door to traffic engineering innovation and makes possible QoS routing with a broader picture of overall network resources. We further argue that SDN can provide more opportunity for the network users to make their own routing selections with network programmability. In this paper, we propose OpenMCR, a general framework for network users to make their own choice of routing given various requirements. OpenMCR provides routing subject to several additive QoS constraints, which is NP-hard when the number of constraints is two or more. By composing various necessary conditions with different path extension schemes, our platform can customize routing solutions for each network user based on their own requirements. Through experiments in an SDN emulated environment, we evaluate multiple aspects of OpenMCR, demonstrate its effectiveness compared with several baselines and validate our theoretical analysis. 
    more » « less
  4. null (Ed.)
    To address the lack of comparative evaluation of Human-in-the-Loop Topic Modeling (HLTM) systems, we implement and evaluate three contrasting HLTM modeling approaches using simulation experiments. These approaches extend previously proposed frameworks, including constraints and informed prior-based methods. Users should have a sense of control in HLTM systems, so we propose a control metric to measure whether refinement operations’ results match users’ expectations. Informed prior-based methods provide better control than constraints, but constraints yield higher quality topics. 
    more » « less
  5. Federated learning (FL) is a popular collaborative learning paradigm, whereby agents with individual datasets can jointly train an ML model. While higher data sharing improves model accuracy and leads to higher payoffs, it also raises costs associated with data acquisition or loss of privacy, causing agents to be strategic about their data contribution. This leads to undesirable behavior at a Nash equilibrium (NE) such as free-riding, resulting in sub-optimal fairness, data sharing, and welfare. To address this, we design MSHAP, a budget-balanced payment mechanism for FL, that admits Nash equilibria under mild conditions, and achieves reciprocal fairness: where each agent's payoff equals her contribution to the collaboration, as measured by the Shapley share. In addition to fairness, we show that the NE under MSHAP has desirable guarantees in terms of accuracy, welfare, and total data collected. We validate our theoretical results through experiments, demonstrating that MSHAP outperforms baselines in terms of fairness and efficiency. 
    more » « less