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.
55
questions
-2
votes
0answers
118 views
Is “paradigm” a word with meaning in syntax or semantics of programming languages? [closed]
I heard that there are different paradigms of programming languages.
I was wondering if "paradigm" is a word with meaning in syntax or semantics of programming languages? If both, when does ...
3
votes
0answers
185 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) ...
1
vote
0answers
99 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 ...
-1
votes
0answers
54 views
How is a divide and conquer recursive algorithm represented in the actor model with lambda calculus?
In Varela's Programming Distributed Computing Systems, Ch4 is about the Actor language which combines the actor model into the lambda calculus.
On p63, it has an example that computes the product of ...
1
vote
2answers
130 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 ...
1
vote
0answers
65 views
Are process calculi (pi calculus, CSP) “shared memory”?
In Andrews' foundations of multithreaded parallel and distributed programming, "shared memory/variable" and "message passing" seem to be opposite programming models, and CSP is ...
3
votes
1answer
83 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 ...
1
vote
0answers
49 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
66 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 ...
5
votes
1answer
198 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 ...
3
votes
1answer
120 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
192 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
1answer
523 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
63 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
97 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
53 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 ...
8
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
130 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 ...
3
votes
1answer
81 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
94 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]. ...
11
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
127 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
110 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
196 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
102 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
135 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
236 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
389 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
184 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 ...
8
votes
1answer
334 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
101 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
557 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
votes
0answers
44 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
253 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
57 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
153 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
107 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
746 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
156 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
134 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
735 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
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?
6
votes
1answer
419 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
208 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
525 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
754 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
478 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 ...
10
votes
1answer
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 ...
5
votes
1answer
339 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 ...
