For the memory model you can take a look at some of the best research in the subfield:
2,560 karma · joined December 10, 2008
twitter: https://twitter.com/johnbender
writing: http://johnbender.us
The example I gave is simple and relates to the example of the parent but there are more complex cases for which it is a matter of ongoing research to define a semantics that also admits compiler optimizations.
For example the "well-defined" semantics of (C|C++)11's atomics admits executions where values can materialize out of thin air [1].
The broader point I was hoping to make is that optimizations are great but are not free in a multi-threaded context with data-races (even benign ones). As a consequence the choice to just remove many of them is one that is supported by many people in the weak-memory community and even appears in newer memory models [2]. For example preventing read-write reorderings to prevent causal cycles.
[1] https://www.cl.cam.ac.uk/~pes20/cpp/notes42.html
[2] http://gee.cs.oswego.edu/dl/html/j9mm.html (ruling out po U rf cycles)
For example, if you're writing a spin-lock, the compiler may lift a read of the lock value out of a loop because, assuming a single thread, the value will never change. This can result in a non-terminating spin-lock. For more see Linux's ACCESS_ONCE.
The example you gave is unfortunate but the consequences of optimizing loops carelessly can be serious.
You may already be aware of this, but that various kinds of temporal logic allows one to capture very complex predicates for the evolution of state machine (much like your person with a dollar).
If you have a familiarity with state machines (here Kripke systems) it might be approachable.
Some useful links:
1. https://www.cs.cmu.edu/~emc/15414-s14/lecture/ModelChecking....
This seems to contradict most of the information I've seen in the diversity reports from companies. Maybe there is some information covering the broader industry that supports this point?
I'm going to see the talk tomorrow at POPL, should be good.
[1] https://hal.archives-ouvertes.fr/hal-01673536/file/Linear%20...
I live about 6 miles from where I work in Los Angeles. I ride my bike (not an E-bike) in three or four times a week. It takes me 25 minutes on average. By contrast, it takes me at least 35 minutes to drive, not including time to park and walk to the office.
I ride on neighborhood roads most of the way for safety, I have to do some personal cleanup when I get there and Los Angeles is particularly bad where traffic is concerned. With all that in mind, it's still worth considering for others in a similar situation.
> Read with pencil and paper in hand, making up little examples for yourself as you go on.
I like to find a difficult question that I can answer with an understanding of the material. This acts as a litmus test of my understanding and a forcing function.
The question can be almost anything, but a general approach I use is to write a "compiler" that maps some concept from the material to a concept I already understand (this normally takes the form of a denotational semantics). Then the question would be, "How can I interpret X as Y?" This technique has its limits since the material can't be too far afield from something I already know and the idea isn't novel but it has been effective for me. The critical bit is forcing myself to write down a fairly comprehensive mapping function. This gets me into the dark corners of my understanding very quickly and adds new questions to answer.
I haven't read too far but I think this refers to the "classic" perspective on proofs which described in "Social Processes and Proofs of Theorems and Programs" [1]. The idea being that proofs should be derivable from first principles even if they are not in practice. This is in contrast to the "probabilistic" perspective which supposes that proofs are only ever "likely" to be correct.
I do a fair amount of work in Coq now and I've done extensive (first order logic) hand written proofs for the same material. So I guess I fall in to the classicist camp. There are a few things I like about this approach as I've experienced it:
Obviously there is no doubt about whether I've proven something. Or at worst there is an absolute minimum of doubt (down to the trusted computing base of Coq and CoC).
With a proof assistant I can easily play with my proof environment and try things out in the same way I do when I'm programming. I suppose this might also be true for more informal proofs but Proof General [2] makes it easy and enjoyable.
Most importantly, I can provide my encodings and proofs as a "library" that others can consume. At first glance this seems to have nothing to do with a classical view of proofs if they exist on paper, but I find higher level proof descriptions in papers hard to consume. Even when the proofs are in my area of expertise. Reading the mathematics fully laid out can be tedious but it contains all the answers to any questions you might have which can't always be said of more informal proofs.
To be fair, my area of expertise (PL) has extensive existing work in Coq and the tool works really well with these kinds of large but "shallow" proofs.
1. https://d1b10bmlvqabco.cloudfront.net/attach/ixkltd3cjy12bv/...
> To take it further, I'm pretty sure if you only absolutely only wanted features for manipulating things
I feel like lisp fits this bill to some degree. Being the AST itself it is "without syntax" to some degree. I wonder if you dislike Lisps? I can't really tell you what this means with regards to our discussion I'm just curious.
> And I, too, like programming language and I feel what makes a language as such cool/useful/etc is that you express a computer's action in a compact, elegant and clear fashion for one's fellow human beings.
Definitely! I would never suggest that we should entirely ignore how the syntax affects our ability to read the code but, to borrow the lisp example again, I don't care about typing lots of parenthesis if I'm otherwise effective.
Again, your earlier comment is not unfounded and I appreciate where you are coming from.
I get that people have syntax preferences and that there's a certain level of "sniff" test that goes along with these things, but as a fan of programming languages I am always interested in the semantics. That is, I'm interested in what's different about this language and its combination of features and goals:
http://clean.cs.ru.nl/Language_features
> The uniqueness typing system of Clean makes it possible to develop efficient applications. In particular, it allows a refined control over the single-threaded use of objects which can influence the time and space behavior of programs. Uniqueness typing can also be used to incorporate destructive updates of objects within a pure functional framework. It allows destructive transformation of state information and enables efficient interfacing to the nonfunctional world (to C but also to I/O systems like X-Windows) offering direct access to file systems and operating systems.
When I read that I think, "Wow! That seems really neat and reminds me of linear types, and I should check this out". Maybe that's just me though.
It's also worth noting that the features page does not mention the word syntax. That's not a deep insight or strong evidence for anything really but it suggests that the designer was interested in the semantics too and that the syntax was a secondary concern.
As for comparison, the C/C++ memory model is more general and is operational. It is also formalized in coq and has some good theorems (data race free sequential consistency being the most obvious).
The RISC memory model is axiomatic and follows the standard axiomatic approach adopted for many other memory models like Java and the current C/C++ standard. That's not a dig, they just don't care as much about rigor.
Axiomatic models consider the every possible execution and then weed out bad ones, where as the operational semantics defines the set of all possible executions using a transition relation. If you're into math you might see these vaguely as extensional and intensional respectively.
It's true that (as implied by the article) you can probably get by with just studying/programming with the C/C++ [1][2] "atomic" memory access types and letting the compiler enforce those semantics, though the reasoning behind a lot of these memory orderings is lost without understanding the motivation/arch. models behind them.
If you're interested in the C/C++ memory models there's active research into specifying them without bad behavior (thin-air reads [3]). Recent results include a semantics that makes value promises and requires a justifying execution [4] which is not totally dissimilar from those required by the official java memory model [5].
1. http://en.cppreference.com/w/cpp/atomic/atomic
2. http://en.cppreference.com/w/c/atomic
3. http://www.cl.cam.ac.uk/~pes20/cpp/notes42.html
4. https://people.mpi-sws.org/~dreyer/papers/promising/paper.pd...
I do proofs and write small programs in coq regularly. I've spent most of my professional life as a web developer.
As with everything learning to do proofs and learning to use Coq are a matter of time, effort, and access to good documentation and other resources.
An invariant that is true of all loop iterations is true of all loop iterations even if the loop diverges. Again, I'm not sure what the implications are for divergence in this setting but it doesn't prevent one from proving loop invariants.
UPDATE: found it thank you.
I'm curious if there is an interpreter written in Gallina that implements the semantics? Maybe with a simulation proof (or similar)? It would be pretty sweet to have a verified interpreter.
Also, found this in the corresponding blog post while search for the Coq source.
> It is Turing incomplete, disallowing unbounded loops and allowing for static analysis
It's definitely possible (and not so hard depending) to do proofs and static analysis of looping programs provided the specification can be encoded as an invariant. To be fair I'm not sure what the implications of non-terminating programs are in this setting and with respect to a specification.
The read/write combinations to the semaphore variable need not be atomic since we know that if this thread is running there are no other threads that can be reading and then modifying it.
MyObject.queueSemaphore = N;
MyObject.emitter = new EventEmitter();
MyObject.queue = function( ... ){
// if this run can take place go
// otherwise wait for a run-complete to try again
if(this.queueSemaphore > 0) {
this.queueSemaphore--;
} else {
// must return a promise that resolves and possibly requeues
return new promise((resolve, reject) => {
this.emitter.once("run-complete", () => {
resolve(true);
});
}).then(() => this.queue( ... ));
}
this.promiseBasedProcess()
// ... work
.finally(() => {
this.queueSemaphore++;
this.emitter.emit("run-complete");
});
}Somewhat useless personal anecdote to follow on this quote that I also liked:
Prior to my PhD studies I had heard of math and experienced it largely as computation. Arithmetic, matrix multiplication, integration by parts etc etc. This is, to my mind, the most terribly boring part of mathematics.
It's not certain, but I suspect that providing at least a few alternate characterizations of mathematics to students stuck doing computations for years and years will almost certainly help some of them find their way to regions of the subject that they find interesting.
> This collection forms an axiom system for the Natural numbers and all true statements are provable in this system. Indeed, every true statement is an axiom.
You have defined the axiom system as the set of all true statements about natural numbers so of course all true statements are provable! But crucially ...
> The problem with doing this is that the collection of all true statements about the Natural numbers is not recursively enumerable.
We want an extensional definition of a set of axioms. One way to get that is to enumerate it! This is important because ...
> Recursively enumerable was the goal of Hilbert and others because they wanted to reduce mathematics to an algorithmic or mechanical process of verification.
I can sympathize with this goal being that I use a proof assistant quite frequently.
Thank you for taking the time to respond!
http://reasoning.cs.ucla.edu/fetch.php?id=136&type=pdf
Abstract:
> We propose the Probabilistic Sentential Decision Diagram (PSDD): A complete and canonical representation of probability distributions defined over the models of a given propositional theory. Each parameter of a PSDD can be viewed as the (conditional) probability of making a decision in a corresponding Sentential Decision Diagram (SDD). The SDD itself is a recently proposed complete and canonical representation of propositional theories. We explore a number of interesting properties of PSDDs, including the independencies that underlie them. We show that the PSDD is a tractable representation. We further show how the parameters of a PSDD can be efficiently estimated, in closed form, from complete data. We empirically evaluate the quality of PSDDs learned from data, when we have knowledge, a priori, of the domain logical constraints.
Still working on my understanding but Professor Darwiche gave a lecture on the material in one of my classes. Salient bit:
> The problem we tackle here is that of developing a representation of probability distributions in the presence of massive, logical constraints. That is, given a propositional logic theory which represents domain constraints, our goal is to develop a representation that induces a unique probability distribution over the models of the given theory.
When I said "true statements that can't be proven" it should have been qualified to a particular set of axioms. That is, I am claiming each set of axioms has it's own set of true but unprovable statements but none have an empty set of those statements. Correct or not?
Based what you say about the second order axioms it seems not, in which case I have some reading to do :)
As far as I'm aware there is work underway to take logical constructions and integrate them with probablistic machine learning to do things like force zero probabilities in impossible input cases. That is encoding domain knowledge into the model directly in the form of symbolic reasoning.
I mean even Bayesian nets require some encoding of causality right? Maybe I'm reading to much of "blah symbolic reasoning is worthless" in your comment?
Another well known project is CompCert the certified C compiler [1]. Which has seen a fair amount of external testing and use in verification of GCC and Clang as a reference for checking invalid compiled semantics [2] (to say nothing of compiling programs).
I'm currently working on my PhD with an emphasis on formal verification (more specifically proofs of correctness) in the weak memory setting.
Some thoughts as I read through:
> Any number of compiler optimizations. For example, our model currently does not account for compiler optimizations that hoist identical stores from both branches of an if statement to precede that statement.
This has until very recently (POPL 2017) been a very serious problem for formal weak memory models. There is only one that I'm aware of for C++11 that avoids the "thin air" read problem that generally arises as a consequence of supporting these types of optimizations. See [1] for more.
> The memory model must be compatible with the hardware that the Linux kernel runs on. Although the memory model can be (and is) looser than any given instance of hardware, it absolutely must not be more strict. In other words, the memory model must in some sense provide the least common denominator of the guarantees of all memory models of all CPU families that run the Linux kernel.
This sort of "lower bound" on bad memory behavior is normally why people target C11 or C++11, but if the author's happen to see this comment I would recommend checking out the work of Karl Crary at CMU [2]. In his model he has omitted the traditional total order on writes present on all modern architectures with the intent of future proofing his semantics.
As a further plug for his semantics, it is not "axiomatic" in the sense of the traditional memory models. Importantly it introduces the notion of programmer specified orders which fits more closely with programmer intuition (by my reckoning) when writing the algorithms than say, the C++11 approach of memory orderings for particular cross thread operations.
In any event an enjoyable read that I will have to come back to later!