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.
56
questions
3
votes
1
answer
49
views
Equivalence of finitary and infinitary semantics of concurrent programs
The following claim is stated on p. 155 of Manna and Pnueli's The Temporal Logic of Reactive and Concurrent Systems: Specification.
Let $P_1$ and $P_2$ be two finitely branching transition systems ...
- 354
0
votes
0
answers
35
views
Do STM transactions using transactional locking need to lock read variables?
I have the same question as in this post: https://dev.to/talhof8/software-transactional-memory-a-stairway-to-lock-free-programming-heaven-194j
In the Transactional Locking II paper, during the "...
4
votes
2
answers
206
views
How exactly does a compatible reduction relation change the $\pi$-calculus?
The reduction relation given for the $\pi$-caculus is usually not compatible (i.e., it's not preserved under arbitrary contexts). Quoting Milner's The Polyadic $\pi$-Calculus: A Tutorial:
It is ...
- 377
0
votes
1
answer
147
views
Where to read about PSO (partial store order) memory model
I have been reading about TSO (total store order) memory models for concurrent programs, but I can not find resources for PSO (partial store order) memory models. Can someone please point to resources....
2
votes
0
answers
295
views
Are CCS and CSP still worth studying?
In Winskel's The formal semantics of programming languages 1993, Ch14 Nondeterminism and parallelism says
This chapter is an introduction to nondeterministic and
parallel (or concurrent) ...
- 639
0
votes
0
answers
505
views
What is the difference between a model of computation and a programming language?
https://en.wikipedia.org/wiki/Model_of_computation includes sequential models, functional models and concurrency models.
Sequential models include finite state machine, Turing machines, random access ...
- 639
1
vote
2
answers
200
views
Can concurrency models be compared in terms of some metrics?
In Seven Concurrency Models in Seven Weeks by Butcher, it compares Actor Model and Communicating Sequential Processes (CSP):
CSP is more flexible than actor model:
In actor model, the medium of ...
- 639
3
votes
1
answer
98
views
Reference request: pi-calculus with simultaneous events
I am interested in using the $\pi$-calculus as a basis for modeling workflows, and came up with an extension that proved useful in my modeling, namely the ability to specify that two or more channel ...
- 420
1
vote
0
answers
54
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 \...
- 2,329
1
vote
0
answers
107
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 ...
- 2,329
5
votes
1
answer
233
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 ...
- 2,329
3
votes
1
answer
127
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 ...
- 161
8
votes
1
answer
294
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, ...
7
votes
1
answer
718
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$-...
- 584
1
vote
2
answers
73
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 ...
- 111
2
votes
1
answer
101
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 ...
- 121
1
vote
0
answers
55
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 ...
- 11
8
votes
3
answers
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 (...
- 501
7
votes
1
answer
144
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,329
2
votes
1
answer
82
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 ...
- 2,329
3
votes
1
answer
102
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]. ...
- 2,329
13
votes
1
answer
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 ...
- 231
3
votes
0
answers
220
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 ...
- 2,329
3
votes
1
answer
114
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,329
-2
votes
1
answer
203
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 ...
- 121
1
vote
1
answer
118
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}: ...
- 2,329
5
votes
0
answers
139
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 ...
- 2,329
3
votes
1
answer
276
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 ...
- 2,329
4
votes
1
answer
427
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, ...
- 141
5
votes
2
answers
197
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 ...
- 161
7
votes
1
answer
494
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 ...
- 83
2
votes
0
answers
105
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 ...
- 2,329
10
votes
2
answers
630
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 ...
- 2,329
1
vote
0
answers
55
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 ...
- 2,329
3
votes
0
answers
265
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 ...
- 2,329
1
vote
0
answers
58
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 ...
- 11
1
vote
1
answer
185
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,329
2
votes
0
answers
110
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.
...
user6973
-1
votes
1
answer
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 ...
- 557
13
votes
1
answer
841
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
0
answers
159
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 ...
- 101
4
votes
0
answers
136
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 ...
- 2,329
1
vote
3
answers
798
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 ...
- 121
23
votes
1
answer
1k
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?
- 551
6
votes
1
answer
437
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 ...
- 161
8
votes
1
answer
216
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 (...
user6973
13
votes
0
answers
533
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)$ ...
- 566
2
votes
0
answers
775
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 ...
- 460
4
votes
1
answer
554
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 ...
- 275
10
votes
1
answer
2k
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 ...
- 203