snu-sf / promising-coq Goto Github PK
View Code? Open in Web Editor NEWThe Coq development of A Promising Semantics for Relaxed-Memory Concurrency
Home Page: https://sf.snu.ac.kr/promise-concurrency/
License: MIT License
The Coq development of A Promising Semantics for Relaxed-Memory Concurrency
Home Page: https://sf.snu.ac.kr/promise-concurrency/
License: MIT License
It is a "call for discussion" for the matter of re-certification.
Currently we allow a thread to take instruction steps as many as it wants, and its promises are re-certified only after all the instruction steps are executed. It basically allows more behaviors, effectively validating more compiler optimizations (e.g. merging a write and a update).
Some people complained that it looks bad, and now we have quite a concrete reason why we don't want it. Consider the following code snippet:
lock(); // implemented w/ acquire CAS to location "l"
x = 1;
unlock(); // implemented as release write to "l"
Here, we want to do some modular reasoning and conclude that x = 1
cannot be promised before the lock is acquired. However, actually it can be, provided that unlock()
is called right before lock()
, as in the certification you can lock()
"l" that is just released by unlock()
. This is basically due to the fact that we re-certify the promises only at the end of a tread step, but not every instruction step, e.g. especially right before lock()
:
// [x = 1] can be promised
unlock();
// not required to re-certify promises here
lock();
x = 1;
unlock();
I believe the benefit of allowing these kind of reasoning is much bigger than the cost of losing some compiler optimizations, which are anyway not performed in the mainstream compilers.
So I propose to revise the promising semantics in such a way that a thread step is really a single instruction step, and the promises are re-certified for each instruction step.
We may need to adjust simulation relations for compiler optimizations, but it should not be a big deal AFAICT. We will see.
Currently, make is called with -j
, which will spawn as many jobs as there are parallel targets at any given time. On systems with (only) 4 CPUs, this leads to unnecessary contention from the ~8 jobs running simultaneously. Additionally, the memory usage far exceeds my modest 8GB of RAM.
I don't quite know how to make an optional -jN
parameter work well with your build.sh setup. In any case, I think it would be safer to not use -j by default.
wf
and consistent
in the Module Configuration
?init
/preservation
propertyCoq 8.9 is out: https://coq.inria.fr/download
@orilahav and I are working on it.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.