# Tag Info

### What's "pseudo time" when used in comparison with semaphores

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

### Is there a mathematical analysis/proof available for correctness of solutions to inter process communication problems?

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 ...
• 1,910
Accepted

### Determinism and pi-calculus

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 ...
• 10.3k
Accepted

### Resources (books, etc) to learn about concurrency theory

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, ...
• 10.3k

### How to design concurrent data structures?

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 ...
• 151

### Can concurrency models be compared in terms of some metrics?

There are no metrics, but an excellent discussion of many concurrency models, in Tony Garnock-Jones PhD thesis. See the (HTML version of the) chapter "Approaches to coordination". This ...
• 1,910

### How exactly does a compatible reduction relation change the $\pi$-calculus?

Interesting question. As Damiano says, while syntactically trivial a change, the π-calculus with non-blocking inputs is a different model of computing. (A very different one, and an extremely ...
• 10.3k

### How exactly does a compatible reduction relation change the $\pi$-calculus?

I don't know "exactly" how it changes the calculus, in the sense that I don't have a formal statement measuring the difference (and I am not aware that there exists one), but allowing ...
• 4,823
Accepted

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 ...
• 1,241

### Under what conditions is the Dining Philosophers Problem unsolvable?

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 ...
• 4,400
Accepted

### Lower bounds and impossibility results for distributed transactions

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 ...
• 2,319

### How to design concurrent data structures?

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 ...
• 21.3k
Accepted

### Concurrent data structures vs. Distributed data structures

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 ...
• 1,241

### Is there a mathematical analysis/proof available for correctness of solutions to inter process communication problems?

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 ...
• 10.8k

### Confusion about a formal definition of PRAM consistency

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 ...
• 4,400
1 vote

### Reference request: pi-calculus with simultaneous events

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 ...
1 vote

### Algorithms to synthesize optimal plans satisfying temporal logic constraints

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

### Why do timeouts require synchronized clocks?

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 ...
• 1,241
1 vote

### How to design concurrent data structures?

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 ...
• 791
1 vote

### Confusions about the technique for verifying implementations of linearizable objects in [Herlihy and Wing, 1990]

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,...
• 800
1 vote
Accepted

### Concurrent transactions satisfying "serializability" but not "snapshot isolation"

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 ...
• 2,319
1 vote

### How can the actor model be applied to allow pure functional languages to have side-effects?

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 ...
• 181

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