25

As it happens, I'm writing a paper about this now. IMO, a good way to think about futures or promises is in terms of the Curry-Howard correspondence for temporal logic. Basically, the idea behind futures is that it is a data structure representing a computation that is in progress, and upon which you can synchronize. In terms of temporal logic, this is the ...


11

Suppose that every circuit of depth $C\log^{k+1} n$ and size $Dn^\ell$ can be converted to an equivalent circuit of depth $C'\log^k n$ and size $D' n^{\ell'}$. Now suppose we are given a circuit of depth $C\log^{k+2} n$ and size $Dn^\ell$, and assume furthermore that it's a levelled circuit (making a circuit levelled only increases the size polynomially). ...


10

I'm one of the authors. Someone pointed me to this question. Based on a quick reading, here's an attempt at answering your concern. What may not be very clear from this version of the description of the simulator (this was the first time I was describing a simulator, and admittedly it reads a bit too much like machine language) is that the view output by ...


9

Is there a set of canonical distributed systems problems from which all the possible distributed system problems can be reduced to? I'm unaware of such a published list of problems. Keep in mind that there are many different (and somewhat incomparable) models in distributed computing, ranging from the "benign" synchronous (fault-free) model where nodes ...


8

What are the advantages of linearizability as a safety property? Are there some results based on this fact in the literature? Suppose that you've implemented a shared memory machine $M$ that only satisfies eventual linearization, defined as follows: in every run $\alpha$ of $M$, there exists some point in time $T_\alpha$, such that linearization holds from ...


7

There are plenty such typing systems. Most work is based on the linear/affine typing system introduced in (1) and generalised in (2). Here are the main works on this subject. In (3) the typing system ensures a precise match with PCF (int its call-by-name variant -- changing to call-by-value is easy). In (4) the typing system gives a precise interpretation ...


7

I believe he may be referring to this paper: NAMING AND SYNCHRONIZATION IN A DECENTRALIZED COMPUTER SYSTEM.


7

There has been various brand of work for formalizing such tricky code. The one I know about are (but I'm no expert on the topic): using "temporal logic" to study distributed systems; one important tool beeing the TLA+ tool is a program that verifies properties of specifications expressed in temporal logic; googling for "TLA+ dining philosopher" links to ...


6

Regarding your first question - safety properties are, in a way, the "easiest" properties to handle, with respect to problems such as model-checking and synthesis. The basic reason for this is that in the automata-theoretic approach to formal methods, reasoning about safety properties reduces to reasoning about finite traces, which is easier than the ...


5

Legally speaking, the term "calculus" is almost always used to describe a language, i.e., a piece of syntax, with added rules of calculation or reasoning. Examples include the good old predicate calculus, lambda calculus, process calculi, various type theories and logics (e.g., Martin-Lof type theory and linear logic). From a programming language point of ...


5

There are not that many books on this subject, as it continues to evolve at a rapid pace. Classic books on process calculi (that don't focus on π-calculus-like mobility) are: C. A. R. Hoare, Communicating Sequential Processes. A. W. Roscoe, The Theory and Practice of Concurrency. M. C. B. Hennessy, Algebraic Theory of Processes. R. Milner, Concurrency ...


5

While I have not read deeply in this area, I found The Art of Multiprocessor Programming by Maurice Herlihy and Nir Shavit to be a helpful introduction and survey of techniques. It explores different algorithms, reasons about how they work and examines the trade-offs, features and limitations of the different approaches. While it has some formalism I ...


3

The arXiv paper "Non-Monotonic Snapshot Isolation" [1] proves several impossibility theorems demonstrating that SI (Snapshot Isolation) and GPR (Genuine Partial Replication) are incompatible. To this end, it first decomposes SI into four properties: Decomposition theorem: $SI = ACA \cap SCONS \cap MON \cap WCF$ where, $ACA$: avoiding cascading aborts;...


3

The answer is not as simple as functional programming. In functional programming here we have a general concept of what is functional programming and the specification of data structures themselves do not change by the fact that they are functional. However that is not the case with concurrency: There are many models of distributed/parallel/concurrent ...


3

You might want to look at the work of Gadi Taubenfeld. Many of his papers deal with impacts of different progress conditions such as (generalized) wait-freedom or obstruction-freedom on the computability power of shared objects in distributed systems, which includes registers.


3

Well, if the philosophers are following the exact same strategy and there is nothing to distinguish them (like who is closest to the door etc.) then they will do exactly the same and deadlock must occur: Whenever one (Aristotle) picks up the left fork then the philosopher on the right (Beauvoir) takes Aristotle's right fork. If you allow access to a source ...


3

What are the big challenges of designing distributed data structures (even harder than those of concurrent data structures)? Some important challenges that practically all distributed data structures face, are handling dynamic changes, implementing a scalable design, and being fault-tolerant. This includes finding answers to questions such as: How can we ...


3

As already suggested above, process algebra or process calculus is the place to start. Quoting freely from the respective Wikipedia page, History In the first half of the 20th century, various formalisms were proposed to capture the informal concept of a computable function, with μ-recursive functions, Turing Machines and the lambda calculus ...


2

You can create a synchronous messaging system with an asynchronous messaging system. This is done by waiting for an acknowledgement directly after sending a message. An example for this is the actor model which is able to build a synchronous messaging system like CSP. But you also can simulate a asynchronous messaging system. When you use buffers to store ...


2

Short answer: yes. Long answer: Using process algebra as a witness to the claimed existential is certainly admissible, but the way the question is phrased might warrant are more direct answer. If TMs are used as mathematical model for sequential computation, we can surely come up with a concurrent version, and show that it is no more powerful than the good ...


2

there is a classic reference/framework increasingly standardized: C.A.R Hoare, Communicating Sequential Processes a 1985 book of same title is now available as ebook with open copyright. wikipedia also has a decent overview note it has some similarity/resemblance to unix pipes/filters there is an implementation in Java, JCSP by Welch/Brown & other ...


2

When they define PRAM (page 11 of the arxiv preprint) they actually state that vis is a partial order (in particular, transitive): We define PRAM consistency by requiring the visibility partial order to be a superset of session order: $$\text{PRAM} \triangleq so \subseteq vis.$$ Thus, the offending arrow in your diagram, from $w(x)0$ to $r(x)0$, is ...


1

Milner defines the SCCS calculus in [1]. This is a generalization of CCS where the actions form an abelian group, and where the communication rule is defined as in my question. [1] Milner, R. Calculi for synchrony and asynchrony. 1983. https://www.sciencedirect.com/science/article/pii/0304397583901147


1

Maybe take a look at http://www.syntcomp.org/ This is a competition of tools solving the LTL synthesis problem (and some related problems).


1

Note that the authors also assume the following: Crucial to our proof is that processing is completely asynchronous; that is, we make no assumptions about the relative speeds of processesor about the delay time in delivering a message. The notion of "timing out processes" refers to the ability of knowing when to conclude that a process must have crashed....


1

The first rule of concurrent data structures is: You do not want concurrency. In the ideal case, distributed/parallel/concurrent computing means that you have a number of completely independent sequential processes. Each process has its own data and resources, and the process is not even aware of any other processes. In the worst case, you have a shared ...


1

Herlihy and Wing write on p. 477: In conclusion, the rep invariant $\mathbf{I}$ must be continually satisfied and the abstraction function continually defined, not only between abstract operations, but also between rep operations implementing abstract operations. The abstraction function maps each rep value to a nonempty set of abstract values: $$ \...


1

Answer my own question: I am not sure with the ideas below. Both comments and answers from experts are highly appreciated. Any references are also welcome. I think the confusion arises from the fact that the two definitions of serializability ($\textrm{SR}$, for short) adopted in [Lin et al@TODS'2009] and [Berenson et al@MSR-TR'1995] are different. The SR ...


1

Erlang is an example. I actually don't know Erlang, so I'm going to use some pseudocode: Suppose you have two threads, Alice and Bob. They talk by calling each other's Send member route, which blocks until the other end replies. Alice can keep some "mutable state" for a single integer as follows: Alice: function main_loop(state): message = Receive() ...


1

I understand the proof as follows. Start with an arbitrary execution of the above algorithm. In this execution each operation on $TS[i]$ and $Val[i]$ has already been linearlized by assuming that these are single-writer multi-reader atomic registers. Therefore, by assumption, the schedule linearizes these low level operations. The remainder of the proof ...


Only top voted, non community-wiki answers of a minimum length are eligible