Questions tagged [concurrency]
Concurrency is the study of systems that operate simultaneously. For example given a set of elevators and a pool of people who want to go to various floors. An example of a concurrent system would be the management system that would tell where the elevators go and where to let off a person of the pool of people.
1
vote
0answers
24 views
How to justify this causally consistent execution in the $(vis, ar)$ framework for distributed consistency models?
In Figure 5.1 of the book "Principles of Eventual Consistency" by Sebastin Burckhardt, 2014, Causal Consistency (CC); wiki is (mainly) defined as the conjunction of $hb \subseteq vis$ and $hb \...
1
vote
0answers
48 views
Confusion about the visibility and arbitration relations in a formal framework for distributed consistency models
In the POPL'14 paper "Replicated Data Types: Specification, Verification, Optimality" and the book "Principles of Eventual Consistency", the authors propose a formal framework for specifying ...
5
votes
1answer
166 views
Confusion about a formal definition of PRAM consistency
I am reading the paper "Consistency in Non-Transactional Distributed Storage Systems" by Paolo Viotti and Marko Vukolić. The authors provide a comprehensive survey of various consistency semantics ...
4
votes
1answer
114 views
Under what conditions is the Dining Philosophers Problem unsolvable?
The wikipedia article for the Dining Philosophers Problem lists some solutions which are dependent on external information, i.e.:
Numbering of forks
A waiter to act as mutex
Messaging between ...
7
votes
1answer
159 views
Resources (books, etc) to learn about concurrency theory
I want to know more about concurrency theory from a formal/mathematical point of view, I know there are a lot of computer science branches that relates to concurrency theory like process algebra, ...
6
votes
1answer
326 views
Determinism and pi-calculus
Milner embedded $\lambda$-calculus into $\pi$-calculus, showing that the $\pi$-calculus is capable of Turing-complete, deterministic calculation. Since parallel compositions of processes in the $\pi$-...
1
vote
2answers
54 views
Algorithms to synthesize optimal plans satisfying temporal logic constraints
I know how NuSMV can be applied on a model to check if certain temporal logic statements are satisfied, particularly LTL. I also know of the LTL to BA conversion routines available online.
I am ...
2
votes
1answer
93 views
Why do timeouts require synchronized clocks?
In Impossibility of distributed consensus with one faulty process @1985 by Fischer at al., the authors state (p375)
We also assume that processes do not have access to synchronized clocks, so ...
1
vote
0answers
50 views
How to read this formula for composition in an asynchronous interaction category?
The paper is available here Interaction Categories and the Foundations of Typed Concurrent Programming Abramsky, Gay, Nagarajan
p.38 composition of two processes $p:A \rightarrow B$, $q:B \rightarrow ...
9
votes
3answers
1k views
How to design concurrent data structures?
I previously asked this question on Programmers.SE, without success.
I'm looking for written learning resources on how to design concurrent data structures. I'm more interested in the design process (...
7
votes
1answer
126 views
Confusions about the technique for verifying implementations of linearizable objects in [Herlihy and Wing, 1990]
In Section 4.3.2 entitled "Proof Method" of
Herlihy and Wing, "Linearizability: A Correctness Condition for Concurrent Objects", 1990
the authors describe the technique for
verifying ...
2
votes
1answer
79 views
How to simulate sequential registers from causal ones?
Background: In distributed shared memory (DSM) model, the problem of register simulations/constructions is to simulate registers with certain characteristic out of registers with weaker features. For ...
3
votes
1answer
93 views
Results about computability power or limitations of shared read/write registers
I want to know more results about the computability power or limitations of shared $\texttt{read/write}$ registers/objects in distributed/concurrent computing theory.
Two typical examples are:
[1]. ...
10
votes
1answer
1k views
What's “pseudo time” when used in comparison with semaphores
I'm currently listening to Alan Kays' talk "Is it really complex or did we just make it complicated ?" (https://www.youtube.com/watch?v=ubaX1Smg6pY&= ) where he says that "semaphores were a bad ...
3
votes
0answers
105 views
In what sense, does a safe register exist?
In the paper "On Interprocess Communication", the author Leslie Lamport have developed a formalism for interprocess communication via shared registers based on lower-level, non-atomic operations and ...
3
votes
1answer
101 views
Lower bounds and impossibility results for distributed transactions
I am studying on distributed transactions, mainly on the correctness criteria (e.g., serializability (SR) and snapshot isolation (SI) in replicated settings) and their implementations.
To avoid ...
-2
votes
1answer
191 views
What are some natural problems that we can quickly find a solution to using massive parallelism but not a canonical solution?
For many problems, more than one output is acceptable. For instance, the problem of finding an assignment that satisfies a boolean formula. If randomness buys us something then it could be that it ...
1
vote
1answer
95 views
Concurrent transactions satisfying “serializability” but not “snapshot isolation”
In [Lin et al@TODS'2009] (Page 5), a history of concurrent transactions satisfying "serializability" ($\textrm{SR}$) but not "snapshot isolation" ($\textrm{SI}$) is given as follows:
$H_{example}: ...
5
votes
0answers
130 views
What is the significance of regarding the mutual exclusion problem as a problem of physics?
In the description of his own paper "On Interprocess Communication" [Distributed Computing 1, 2 (1986), 77-101], Leslie Lamport wrote
Most computer scientists regard synchronization problems, such ...
3
votes
1answer
223 views
Concurrent data structures vs. Distributed data structures
In the context of multi-processor/multi-threaded systems, there are plenty of well-studied concurrent data structures, including stacks, queues, linked lists, etc. Here is an excellent survey on ...
4
votes
1answer
349 views
How can the actor model be applied to allow pure functional languages to have side-effects?
I just read this blog post which argues that monads might be too obscure or difficult to understand as the default "interface to the impure world" in purely functional programming languages; instead, ...
5
votes
2answers
178 views
Is there a mathematical analysis/proof available for correctness of solutions to inter process communication problems?
I've been going over some material related to IPC recently from Tanenbaum's "Modern Operating Systems" and revisited semaphore after many years. There is a lot of code and pseudo code based ...
7
votes
1answer
221 views
Non uniform NC-hierarchy collapse?
Jianer Chen's paper "Characterizing parallel hierarchies by reducibilities" Information Processing Letters 39(1991) 303-307 shows the theorem:
If $NC^{k+1} = NC^k$ then we have $NC = NC^k$
His proof ...
2
votes
0answers
97 views
Are the sets of executions of data-race free programs equal, when run on causal memory and on sequentially consistent memory respectively?
In the paper "Causal Memory: Definitions, Implementations, and Programming (Distributed Computing [DC] 1995)", the authors present a formal definition of causal memory, an abstraction of distributed ...
10
votes
2answers
446 views
Why is linearizability a safety property and why are safety properties closed sets?
In Chapter 13 "Atomic Objects" of the book "Distributed Algorithms" by Nancy Lynch, linearizability (also known as atomicity) is proved to be a safety property. That is to say, its corresponding trace ...
1
vote
0answers
39 views
What is the staleness in this execution of the $k$-atomic multi-writer register construction from $k$-atomic single-writer ones?
Background:
$K$-atomicity is a consistency condition meaning that a read operation can return one of the values written by the last $k$ preceding writes in an order consistent with real time. It is a ...
3
votes
0answers
233 views
Atomic snapshot algorithms on tree-structured shared registers
Background:
Atomic snapshot memory is a shared memory partitioned into words written (updated) by individual processes, or instantaneously read (scanned) in its entirety.
The Gang of Six algorithm ...
1
vote
0answers
55 views
Correct algorithms with sequentially inconsistent executions
as far as I understood one wants that an algorithm produces only results that can be also achieved by a sequentially consistent execution.
My question is whether this is true or whether there are ...
1
vote
1answer
140 views
Should the Schedule of ``High-level Operations'' Respect the Linearizability of ``Low-level Operations'' in Proof of Simulation Algorithm?
Backgroud
I am reading Chapter 10 ``Fault-Tolerant Simulations of Read/Write Objects'' of the Book Distributed Computing (by Hagit Attiya & Jennifer Welch). Specifically, in section 10.2.3, it ...
2
votes
0answers
105 views
non-malleable commitment and security parameters
Although it is not clear, it appears that definition 5 of this paper,
page 10 of this paper, and page 6 of this paper, each assume
that the honest parties will all use the same security parameter.
...
-1
votes
1answer
2k views
synchronous vs. asynchronous message passing
I think I remember a claim that asynchronous message passing can be implemented by synchronous message passing but not vice versa. Unfortunately, I don't remember an article name, an author, or even a ...
13
votes
1answer
659 views
Is there a list of canonical problems in distributed systems?
Last week, I was reading again Leslie's Lamport's 1982 trasncript of a conference he gave about Solved Problems, Unsolved Problems and Non-Problems in Concurrency. The paper is easily readable, but ...
0
votes
0answers
146 views
Sequential Consistency, cannot find a sufficient explanation
I am having a hard time understanding the SC memory model properly.
The sentence "the result of any execution is the same as if the operations of all the processors were executed in some sequential ...
4
votes
0answers
127 views
What are the parts of consistency model playing in hardware, operating system, and programming language?
In multiprocessor programming, consistency model is the key concept to express the correctness of concurrent objects ranging from simple read/write shared variable to concurrent data structures like ...
1
vote
3answers
682 views
Does mathematical model for conccurent computations exist?
Turing machines can represent any computation. Can they also represent concurrent computations? Eg. multiple computations that can happen at the same time?
If yes, how are the concurrent computations ...
22
votes
1answer
963 views
How are Futures described in terms of category theory?
Is there a useful description of futures or promises in terms of category theory? In particular, what could the categorical dual of Future be?
6
votes
1answer
402 views
Semantics of concurrent languages
I've seen that the preferred way to specify the semantics of a concurrent language is to use a process calculus (e.g. pi calculus, join calculus). But in the paper presenting the F# asynchronous ...
8
votes
1answer
199 views
question about concurrent ZK paper by Prabhakaran & Sahai
Concurrent Zero Knowledge Proofs with Logarithmic
Round-Complexity
Page numbers are from the paper itself, and not the pdf.
From page 3,
"An interactive proof system is said to be black-box (...
13
votes
0answers
520 views
Lock-free, constant update-time concurrent tree data-structures?
I've been reading a bit of the literature lately, and have found some rather interesting data-structures.
I have researched various different methods of getting update times down to $\mathcal{O}(1)$ ...
2
votes
0answers
706 views
On the Bakery Mutual exclusion Algorithm
Lamport's Bakery Algorithm is one of the most elegant algorithms for mutual exclusion. The beauty of it is that it works even when the underlying system only provides a weak form of registers called ...
4
votes
1answer
434 views
Are the Actor Model and Process Algebra “equivalent”?
I often see casual mention that the Hewit/Agha Actor Model is equivalent in capability to process algebra, like CSP, CCS and ACP. Ie, one can be implemented in the other. Is there a paper that ...
9
votes
1answer
1k views
A practical multi-word compare-and-swap operation
In the paper with the same title as that of this question, the authors describe how to build a nonblocking linearizable multi-word CAS operation using only a single-word CAS. They first introduce the ...
5
votes
1answer
318 views
Definition of a hereditary relation
Sassone, V., Nielsen, M. and Winskel, G. (1996) Models for Concurrency: Towards a Classification. Theoretical Computer Science, 170 (1-2). pp. 297-348., p. 307:
Given a tree $S$, define … $\#$ is ...
8
votes
3answers
5k views
Difference between Strict Consistency and Sequential Consistency
I understand strict and sequential consistency independently fairly well.
Strict C basically enforces the actual order in which the instructions ran on the global clock.
Sequential Consistency ...
10
votes
2answers
420 views
Limits on lock-free collections?
David Rodríguez - dribeas wrote in a comment on StackOverflow that "Not all collections can be implemented without locks". I'm not sure if this is true, and I can't find proof either way.
This ...
24
votes
2answers
525 views
Parallel Dynamic Search
Is there a natural parallel analog to red-black trees with similar or even not-terribly-worse properties for updates while being reasonably work-efficient ?
More generally, what's the best we can do ...
25
votes
1answer
4k views
What's the difference between the Actor Model of Concurrency and Communicating Sequential Processes
I'm trying to wrap my head around what the real differences between the Actor Model of concurrency and Communicating Sequential Processes (CSP) model of concurrency.
So far the best that I have ...
8
votes
1answer
182 views
Process modeling with fine-grained notions of location
Is anyone aware of any process algebraic (or related) formalisms that capture fine-grained location information? I'm familiar with ambients and bigraphs, which obviously have a location model, but ...
