-
Lessons Learned from Efforts to Standardize Streaming In SQL
Authors:
Sabina Petride,
Dan Sotolongo,
Jan Michels,
Andrew Witkowski,
Cara Haas,
Jim Hughes
Abstract:
Acknowledging the reality of streaming languages and platforms overlap** with SQL and database systems, in 2019 INCTIS Data Management established an Expert Group with the focused mission to initiate the process of standardizing streaming support in SQL. Over time, the roster included companies like Actian, Alibaba, Amazon Web Services, Confluent, dbt Labs, Google, Hazelcast, IBM, Materialize, M…
▽ More
Acknowledging the reality of streaming languages and platforms overlap** with SQL and database systems, in 2019 INCTIS Data Management established an Expert Group with the focused mission to initiate the process of standardizing streaming support in SQL. Over time, the roster included companies like Actian, Alibaba, Amazon Web Services, Confluent, dbt Labs, Google, Hazelcast, IBM, Materialize, Microsoft, Oracle, Snowflake, SQLstream and Timeplus. For the span of more than one year, representatives of each company have presented key features of their streaming product or, in some cases, multiple streaming products. These were live technical Q&A sessions accompanied by summary or position papers, which are unquestionably valuable. As expected, substantial time was spent in clarifying what common terms meant in each system and setting up a glossary. These sessions were followed by clarification notes and debates, and decisions that appeared mandatory to allow further progress. This first phase was followed by the next phase, which consisted of the group meetings, in which the expert group (EG) agreed on main exit criteria topics that a streaming solution in SQL must address, and position papers and follow-ups were written and discussed. This paper summarizes these group efforts, up to the summer of 2023.
△ Less
Submitted 6 November, 2023;
originally announced November 2023.
-
Knowledge-Based Synthesis of Distributed Systems Using Event Structures
Authors:
Mark Bickford,
Robert Constable,
Joseph Halpern,
Sabina Petride
Abstract:
To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. This process is particularly effective if the specifications are written in a high-level language that makes it easy for designers to specify their goals. We consider a high-level specification language that results from a…
▽ More
To produce a program guaranteed to satisfy a given specification one can synthesize it from a formal constructive proof that a computation satisfying that specification exists. This process is particularly effective if the specifications are written in a high-level language that makes it easy for designers to specify their goals. We consider a high-level specification language that results from adding knowledge to a fragment of Nuprl specifically tailored for specifying distributed protocols, called event theory. We then show how high-level knowledge-based programs can be synthesized from the knowledge-based specifications using a proof development system such as Nuprl. Methods of Halpern and Zuck then apply to convert these knowledge-based protocols to ordinary protocols. These methods can be expressed as heuristic transformation tactics in Nuprl.
△ Less
Submitted 19 May, 2011; v1 submitted 23 June, 2009;
originally announced June 2009.
-
A Knowledge-Based Analysis of Global Function Computation
Authors:
Joseph Y. Halpern,
Sabina Petride
Abstract:
Consider a distributed system N in which each agent has an input value and each communication link has a weight. Given a global function, that is, a function f whose value depends on the whole network, the goal is for every agent to eventually compute the value f(N). We call this problem global function computation. Various solutions for instances of this problem, such as Boolean function comput…
▽ More
Consider a distributed system N in which each agent has an input value and each communication link has a weight. Given a global function, that is, a function f whose value depends on the whole network, the goal is for every agent to eventually compute the value f(N). We call this problem global function computation. Various solutions for instances of this problem, such as Boolean function computation, leader election, (minimum) spanning tree construction, and network determination, have been proposed, each under particular assumptions about what processors know about the system and how this knowledge can be acquired. We give a necessary and sufficient condition for the problem to be solvable that generalizes a number of well-known results. We then provide a knowledge-based (kb) program (like those of Fagin, Halpern, Moses, and Vardi) that solves global function computation whenever possible. Finally, we improve the message overhead inherent in our initial kb program by giving a counterfactual belief-based program that also solves the global function computation whenever possible, but where agents send messages only when they believe it is necessary to do so. The latter program is shown to be implemented by a number of well-known algorithms for solving leader election.
△ Less
Submitted 23 July, 2007;
originally announced July 2007.
-
Expressing Security Properties Using Selective Interleaving Functions
Authors:
Joseph Y. Halpern,
Sabina Petride
Abstract:
McLean's notion of Selective Interleaving Functions (SIFs) is perhaps the best-known attempt to construct a framework for expressing various security properties. We examine the expressive power of SIFs carefully. We show that SIFs cannot capture nondeducibility on strategies (NOS). We also prove that the set of security properties expressed with SIFs is not closed under conjunction, from which i…
▽ More
McLean's notion of Selective Interleaving Functions (SIFs) is perhaps the best-known attempt to construct a framework for expressing various security properties. We examine the expressive power of SIFs carefully. We show that SIFs cannot capture nondeducibility on strategies (NOS). We also prove that the set of security properties expressed with SIFs is not closed under conjunction, from which it follows that separability is strictly stronger than double generalized noninterference. However, we show that if we generalize the notion of SIF in a natural way, then NOS is expressible, and the set of security properties expressible by generalized SIFs is closed under conjunction.
△ Less
Submitted 3 August, 2006;
originally announced August 2006.
