johnbender

9 ms·

61.
by johnbender 9y ago
I somehow just noticed that this article was partly authored by Jade Alglave and others who will certainly be aware of the papers I linked.
62.
by johnbender 9y ago
[cross posted from the article comments section] 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 nu
63.
by johnbender 9y ago
"Lowering" (though I've never heard it called that) is also handy in the course of working with formal semantics especially in the case of proofs and other serious reasoning. You can "port" your reasoning from the &
64.
by johnbender 10y ago
> in my experience program committees generally regard difficulty as a negative for a paper. I don't know if we're talking about the same type of difficulty. I don't think program committees see the difficulty of the probl
65.
by johnbender 10y ago
Here are my thoughts based on my experience with peer reviewed publication. There are two high level criteria for publication: novelty and difficulty (this is in my field of Programming Languages and Systems so keep that in mind). The novel
66.
by johnbender 10y ago
> It's depressing but there are many places where people prefer to use Hipchat and Slack I'm not sure this is bad in an absolute sense. If I'm working on something, the semi-asynchronous nature of chat (assuming disabled n
67.
by johnbender 10y ago
I read this (possibly wrongly) to be a proxy for "unencumbered page load speed" which is a feature that many users value beyond the 1% who care about noscript.
68.
by johnbender 10y ago
Quantum Computing for Computer Scientists Note, you have to be willing to put the time in, especially if your linear algebra is rusty or (like me) you have only a passing familiarity with complex numbers. With that in mind, it's almost
69.
by johnbender 10y ago
> Pierce's Types and Programming Languages Pierce's book is as approachable as you're likely to see with respect to type systems. You mostly just have to dig in.
70.
by johnbender 10y ago
I've built interpreters for both a subset of Java and a full Lisp. Here's my take. > Is there something inherently easier to implementing a functional language instead of something more imperative? Other answers have focused on
71.
by johnbender 10y ago
Thank you!
72.
by johnbender 10y ago
Shu, The concurrency/memory model nerds out here would love to see an early draft if at all possible :) If nothing else, is it going to be weaker than sequential consistency?
73.
by johnbender 10y ago
I would go further. Given the sums of money involved I think it might also be worthwhile to have a formal semantics and a logic for proving safety properties of these blockchain programs (beyond type safety). Not every application would req
74.
by johnbender 10y ago
Can anyone familiar with the linked material comment on whether there is a standard model used in the proofs there and in the DS literature? I'm thinking of something like Lamport's global time model from "On interprocess com
75.
by johnbender 10y ago
Lambda lifting!
76.
by johnbender 10y ago
Do you know if they address I/O reordering within the scheduler? For example transaction implementations often require that writes (distinct file system calls) hit the disk in a particular order to guarantee a sane state for the databa
77.
by johnbender 10y ago
Backups don't help if writes don't make it to disk in the order and manner expected by the application programmer. There's an emerging consensus that there are crash protocol bugs lurking everywhere due to I/O scheduler
78.
by johnbender 10y ago
Event assuming that you can look at the source code for your filesystem/kernel the results of a given write still depend on the conditions and orders under which your writes hit disk relative to other processes' writes. For exampl
79.
by johnbender 11y ago
> The difference between the top riders is so slim that it would without question Exactly. In the first clip you posted, at the end in the tour of flanders when Cancellara attacks before the finish, neither his cadence nor his body posit
80.
by johnbender 11y ago
In many cases trading in non-deterministic choice for deterministic choice (ie, parsing expression grammars) makes reasoning about and writing grammars much easier. For example, in the case of the arithmetic expressions grammar the rules sh
81.
by johnbender 11y ago
To add just a bit more: When assignments to variables happen in the context of a procedure call it's preferable to use registers for performance reasons since memory access (even cache) is much slower by comparison. Unfortunately regis
82.
by johnbender 11y ago
http://plv.mpi-sws.org/rustbelt/ As part of defining the Rust semantics they will certainly tackle the question of the memory model. Dreyer and company have a track record of providing semantics and reasoning principle
83.
by johnbender 11y ago
Assuming you mean the weak memory models, the compiler normally enforces the guarantees made by the semantics of the programming language ... assuming you have a semantics. That's where this project comes in and that is why the C++ mem
84.
by johnbender 11y ago
One can also calculate the derivative of a context free grammar with respect to a given terminal. http://matt.might.net/articles/parsing-with-derivatives/
85.
by johnbender 11y ago
> Constraint programming allows you to write the specification of your program This captures the core idea from my brushes with various constraint based programming languages. There's nearly always a spec floating around somewhere,
86.
by johnbender 11y ago
It's worth noting that this is a peer reviewed conference publication (in POPL no less). So, despite the title a lot of time and thought has gone into the content.
87.
by johnbender 11y ago
A "memory model" and "memory management" are two different things. Memory management normally conotes the process for allocation and reclamation of memory in a program. A memory model defines where reads can get their in
88.
by johnbender 11y ago
NP-completeness for automatic fence placement between two specified instructions in the presence of arbitrary goto statements. Reduction is from negation free 2-SAT to control flow graphs for real programs. Didn't make it into my first
89.
by johnbender 12y ago
I was wondering if concolic execution [1] isn't more popular for this type of thing due to the difficulty in setting up the tools or relative newness compared to randomly generating inputs? 1. http://en.wikipedia.org/wi
90.
by johnbender 12y ago
It doesn't look like the LOCK prefix applies to MOV (from a quick google)? So how does it address write buffering or OOE for stores in a TSO memory model? [edit] "never require the hammer of mfence for correct synchronization&quot

More ›