8 votes

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.
user avatar
7 votes

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 ...
user avatar
  • 1,910
7 votes
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 ...
user avatar
6 votes
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, ...
user avatar
5 votes

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 ...
user avatar
5 votes

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 ...
user avatar
  • 1,910
3 votes

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 ...
user avatar
3 votes

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 ...
user avatar
3 votes
Accepted

Results about computability power or limitations of shared read/write registers

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 ...
user avatar
  • 1,241
3 votes

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 ...
user avatar
3 votes
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 ...
user avatar
  • 2,319
3 votes

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 ...
user avatar
  • 21.3k
3 votes
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 ...
user avatar
  • 1,241
2 votes

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 ...
user avatar
  • 10.8k
2 votes

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 ...
user avatar
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 ...
user avatar
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).
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
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,...
user avatar
  • 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 ...
user avatar
  • 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 ...
user avatar
  • 181

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