4 ms·

> One of the main breakthroughs of CertiKOS is that it supports concurrency, meaning that it can simultaneously run multiple threads (small sequences of program

> One of the main breakthroughs of CertiKOS is that it supports concurrency, meaning that it can simultaneously run multiple threads (small sequences of programmed instructions) on multiple central processing unit (CPU) cores. Isn't this parallelism?

crocal 10y ago
It is. The point here is that they have proven that this feature is hack-proof. This is extremely difficult. The article does not give much details, however, Andrew Appel is a very big name in the field.
dvirsky 10y ago
> “Ten years ago, no one would predict that we could prove the correctness of a single-threaded kernel, much less a multi-core one." So apparently it's a breakthrough in this context.
sriram_malhar 10y ago
Yes, having access to multiple cores means that one can process some things faster. But performance is not the focus of this work, although that is a happy side effect. The focus is on correctness of concurrent code. CertiKOS's model explicitly accounts for the presence of concurrent processors accessing memory in an arbitrarily interleaved fashion. In order to get the verification process to sign off on a particular architecture, all accesses to shared memory _must_ use the correct synchronization primitives and memory barriers, among other things.
glastra 10y ago
Yes, I've seen them used as synonyms, even when, in my opinion, they are not. For the record, what I (and others, and I assume the parent too) understand as concurrency is many threads in a single core (interleaved/evicted, scheduling, quanta, yadda yadda), while parallelism means running multiple tasks in multiple cores at once.
- naasking 10y ago
  > For the record, what I (and others, and I assume the parent too) understand as concurrency is many threads in a single core (interleaved/evicted, scheduling, quanta, yadda yadda), while parallelism means running multiple tasks in multiple cores at once. In computer science, concurrency is a system of non-deterministic interleaved components, parallelism is a deterministic performance enhancement for programs by running fragments of it simultaneously. For the purposes of verification, non-deterministic interleaving is the truly challenging problem, so the paper's use of "concurrency" seems reasonable.
BraveNewCurency 10y ago
https://www.youtube.com/watch?v=cN_DpYBzKso https://www.youtube.com/watch?v=cN_DpYBzKso Rob Pike's talk on why 'Concurrency Is Not Parallelism'
- BraveNewCurency 10y ago
  Oops, that may not have been your question.

crocal 10y ago

It is. The point here is that they have proven that this feature is hack-proof. This is extremely difficult. The article does not give much details, however, Andrew Appel is a very big name in the field.

dvirsky 10y ago

> “Ten years ago, no one would predict that we could prove the correctness of a single-threaded kernel, much less a multi-core one." So apparently it's a breakthrough in this context.

sriram_malhar 10y ago

Yes, having access to multiple cores means that one can process some things faster. But performance is not the focus of this work, although that is a happy side effect. The focus is on correctness of concurrent code. CertiKOS's model explicitly accounts for the presence of concurrent processors accessing memory in an arbitrarily interleaved fashion. In order to get the verification process to sign off on a particular architecture, all accesses to shared memory _must_ use the correct synchronization primitives and memory barriers, among other things.

glastra 10y ago

Yes, I've seen them used as synonyms, even when, in my opinion, they are not. For the record, what I (and others, and I assume the parent too) understand as concurrency is many threads in a single core (interleaved/evicted, scheduling, quanta, yadda yadda), while parallelism means running multiple tasks in multiple cores at once.

naasking 10y ago
> For the record, what I (and others, and I assume the parent too) understand as concurrency is many threads in a single core (interleaved/evicted, scheduling, quanta, yadda yadda), while parallelism means running multiple tasks in multiple cores at once. In computer science, concurrency is a system of non-deterministic interleaved components, parallelism is a deterministic performance enhancement for programs by running fragments of it simultaneously. For the purposes of verification, non-deterministic interleaving is the truly challenging problem, so the paper's use of "concurrency" seems reasonable.

BraveNewCurency 10y ago

https://www.youtube.com/watch?v=cN_DpYBzKso https://www.youtube.com/watch?v=cN_DpYBzKso Rob Pike's talk on why 'Concurrency Is Not Parallelism'

BraveNewCurency 10y ago
Oops, that may not have been your question.