2 Search Results for "McSherry, Frank"


Document
Verified Progress Tracking for Timely Dataflow

Authors: Matthias Brun, Sára Decova, Andrea Lattuada, and Dmitriy Traytel

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)


Abstract
Large-scale stream processing systems often follow the dataflow paradigm, which enforces a program structure that exposes a high degree of parallelism. The Timely Dataflow distributed system supports expressive cyclic dataflows for which it offers low-latency data- and pipeline-parallel stream processing. To achieve high expressiveness and performance, Timely Dataflow uses an intricate distributed protocol for tracking the computation’s progress. We modeled the progress tracking protocol as a combination of two independent transition systems in the Isabelle/HOL proof assistant. We specified and verified the safety of the two components and of the combined protocol. To this end, we identified abstract assumptions on dataflow programs that are sufficient for safety and were not previously formalized.

Cite as

Matthias Brun, Sára Decova, Andrea Lattuada, and Dmitriy Traytel. Verified Progress Tracking for Timely Dataflow. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 10:1-10:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{brun_et_al:LIPIcs.ITP.2021.10,
  author =	{Brun, Matthias and Decova, S\'{a}ra and Lattuada, Andrea and Traytel, Dmitriy},
  title =	{{Verified Progress Tracking for Timely Dataflow}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{10:1--10:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2021.10},
  URN =		{urn:nbn:de:0030-drops-139057},
  doi =		{10.4230/LIPIcs.ITP.2021.10},
  annote =	{Keywords: safety, distributed systems, timely dataflow, Isabelle/HOL}
}
Document
Differentially Private Combinatorial Optimization

Authors: Kunal Talwar, Anupam Gupta, Katrina Ligett, Frank McSherry, and Aaron Roth

Published in: Dagstuhl Seminar Proceedings, Volume 9511, Parameterized complexity and approximation algorithms (2010)


Abstract
Consider the following problem: given a metric space, some of whose points are ``clients,'' select a set of at most $k$ facility locations to minimize the average distance from the clients to their nearest facility. This is just the well-studied $k$-median problem, for which many approximation algorithms and hardness results are known. Note that the objective function encourages opening facilities in areas where there are many clients, and given a solution, it is often possible to get a good idea of where the clients are located. This raises the following quandary: what if the locations of the clients are sensitive information that we would like to keep private? emph{Is it even possible to design good algorithms for this problem that preserve the privacy of the clients?} In this paper, we initiate a systematic study of algorithms for discrete optimization problems in the framework of differential privacy (which formalizes the idea of protecting the privacy of individual input elements). We show that many such problems indeed have good approximation algorithms that preserve differential privacy; this is even in cases where it is impossible to preserve cryptographic definitions of privacy while computing any non-trivial approximation to even the emph{value} of an optimal solution, let alone the entire solution. Apart from the $k$-median problem, we consider the problems of vertex and set cover, min-cut, facility location, and Steiner tree, and give approximation algorithms and lower bounds for these problems. We also consider the recently introduced submodular maximization problem, ``Combinatorial Public Projects'' (CPP), shown by Papadimitriou et al. cite{PSS08} to be inapproximable to subpolynomial multiplicative factors by any efficient and emph{truthful} algorithm. We give a differentially private (and hence approximately truthful) algorithm that achieves a logarithmic additive approximation. Joint work with Anupam Gupta, Katrina Ligett, Frank McSherry and Aaron Roth.

Cite as

Kunal Talwar, Anupam Gupta, Katrina Ligett, Frank McSherry, and Aaron Roth. Differentially Private Combinatorial Optimization. In Parameterized complexity and approximation algorithms. Dagstuhl Seminar Proceedings, Volume 9511, pp. 1-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)


Copy BibTex To Clipboard

@InProceedings{talwar_et_al:DagSemProc.09511.6,
  author =	{Talwar, Kunal and Gupta, Anupam and Ligett, Katrina and McSherry, Frank and Roth, Aaron},
  title =	{{Differentially Private Combinatorial Optimization}},
  booktitle =	{Parameterized complexity and approximation algorithms},
  pages =	{1--31},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9511},
  editor =	{Erik D. Demaine and MohammadTaghi Hajiaghayi and D\'{a}niel Marx},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.09511.6},
  URN =		{urn:nbn:de:0030-drops-24986},
  doi =		{10.4230/DagSemProc.09511.6},
  annote =	{Keywords: Differential Privacy, Approximation Algorithms}
}
  • Refine by Author
  • 1 Brun, Matthias
  • 1 Decova, Sára
  • 1 Gupta, Anupam
  • 1 Lattuada, Andrea
  • 1 Ligett, Katrina
  • Show More...

  • Refine by Classification
  • 1 Computing methodologies → Distributed algorithms
  • 1 Security and privacy → Logic and verification
  • 1 Software and its engineering → Data flow languages

  • Refine by Keyword
  • 1 Approximation Algorithms
  • 1 Differential Privacy
  • 1 Isabelle/HOL
  • 1 distributed systems
  • 1 safety
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2010
  • 1 2021

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail