buttproblem
I'm wondering because I've been studying building automated program reasoning tools and have found that even just creating the call-graph is difficult: I imagine the end result potentially confusing the user because it is either incomplete or overly pessimistic. For example, the LLVM call-graph (apart from not being in the language directly used by the developer) does not include edges from indirect calls because their targets cannot be resolved (so it is incomplete). Alternatively, in the case where you don't know which function is called you can just add an edge to every function in the program (pessimistically).
The same story goes for the dependency graph.
I myself am a bit pessimistic myself about more powerful software understanding tools probably because I've been working on the problem for too long. It's particularly difficult because the languages end up being too difficult to analyze, and there is a huge engineering effort in creating an analyzer which is tuneable to handle various language features efficiently. But, if you have a particular problem and a particular (subset) of the language it ends up working nicely.
Some interested related work is Delta Debugging. Here, an automated tool runs a set of tests and uses slicing to narrow down statements in the program causing the bug. The gist of this is to look at the statements which occur on every failing execution and then present these to the end user. More tests causing the error will usually lead to a smaller explanation.
The paper here presented a dynamic slicing technique. The problem with dynamic slicing is runtime overhead. The most naive approach is to log the operands and output of every instruction in the program which is quite expensive. Traces for real world programs will probably be many gigabytes. I don't have any numbers off the top of my head. But you could not deploy the instrumented version of the program for slicing to your users without it degrading performance. Intel recently added some hardware tracing to their processors which might offset this.
The alternative is static slicing where the program is not actually executed. Here, you give the slicer the statement of interest (e.g., a line of code where a seg fault occurred) and it will give you back the statements involved in the computation, same as in dynamic slicing. The problem here is accuracy. It's difficult and expensive to know what a program does before executing it (e.g., what memory locations could be accessed by this location? What is the value of the index used to access this array). So, the slice is often too large, or the slicing algorithm is too complicated and fails to terminate in a reasonable time on a real program.
Of course for hard to diagnose bugs you could use techniques such as this, and maybe it would be beneficial. It's hard to way the cost of wrangling with a slicing tool versus just staring at the code and trying to figure it out yourself. There's many more similar debugging techniques which are also quite interesting (e.g., program synthesis to automatically find and repair bugs, using slicing with test case generation (e.g., fuzzing, symbolic execution) to focus towards particular code regions) but these are probably even more research-y and hard to use in practice.
As a concrete example, interactive theorem provers can prove the termination of Paxos for an arbitrary number of nodes (i.e., a system of `n` nodes will reach consensus, where `n` is a positive integer). But, automatically generating such a proof for something as complicated and parameterized as Paxos is an open problem ([1] describes an automatic tool working toward that goal).
Another thing to keep in mind is the goal of the tool: verification versus bug hunting. Verification aims to prove that a property will never be violated, while bug hunting aims to find a property violation. Here's a list of some types of tools off the top of my head.
Bounded model checkers such as CBMC [2] essentially search the entire state-space of the program; you can conceptually think of this as searching through a graph which has some start node, and you'd like to find a path from the start to an error. This is a bug hunting technique since the software/hardware may have an infinite state space (e.g., `while (true) ++i`), hence the search space must be bounded (e.g., unroll loops). For finite-state systems this can generate proofs of correctness. For infinite state systems, it can generate proofs up to a certain bound (e.g., correct for some number of clock cycles, correct for some number of loop iterations). The benefit of bounded model checkers is that when they find an error they generate a counter-example, which is essentially inputs to the program causing it to fail. So, you could use the counter-example as a concrete test case to fix the issue. Techniques such as counter-example guided abstraction refinement, and more recently IC3 and property-directed reachability make use of these counter-examples to generate proofs for infinite state systems.
A complementary technique is abstract interpretation, and numerical abstract interpretation in particular. One successful tool is Astree, though closed source, has been used to verify properties on Airbus planes. Abstract interpretation is complementary to something like bounded-model checking since it can be used to verify properties on infinite state systems. Numerical abstract interpretation can be used to generate numerical proofs such as, "on line 10, variable `x` is in the range `[-10, 10]`, or constraints between variables such as `x - y >= 10`. A difficult part with abstract interpretation, however, is that when it reports an error it may be the case that the error is a false-alarm and it doesn't actually exist. You can think of numerical abstract interpretation as typical "compiler algorithms" such as constant propagation but keeping track of much more complicated information.
Symbolic/Concolic execution, such as KLEE [4], Pex and Moles [5], and their successor IntelliTest [6], are sort of a middle ground between model checking, and traditional unit testing (i.e., hand writing inputs to the program to test it). The main goal is to automatically generate such tests in order to test behavior in the program (e.g., generate a set of test inputs to have 100% code coverage). The modern versions of these techniques make use of dynamic information (i.e., they actually execute the program under test), and use this information to make decisions about future executions. More concretely, you can imagine the program executing past some branch `if (c)` which was not taken (i.e., `c == false`) and then, the analysis asks the question: "what do the program inputs need to be such that `c == true`. An answer to this question generates new inputs and allows another test to be generated and explored.
Stateless model checking is another automated dynamic technique [7,8,9] used to explore non-determinism in concurrent programs. Essentially, it automatically generates "test cases" (i.e., new thread schedules) to efficiently explore the state space caused by a non-deterministic scheduler.
And there's a bunch of other techniques out there too (e.g., symbolic model checking). There's also a huge amount of work on practical test input generation for hardware. On top of all these techniques, there are there applications to solving specific problems, and heuristics to make them more practical and scalable. Overall, most of the techniques are niche and not widely used, but have been applied in various areas.
[1] https://www7.in.tum.de/~gleissen/papers/sharpie.pdf
[2] http://www.cprover.org/cbmc/
[5] https://www.microsoft.com/en-us/research/project/pex-and-mol...
[6] https://www.visualstudio.com/vs/release-notes/#Testing
[7] https://github.com/markus-kusano/SysTest
[8] http://www.srl.inf.ethz.ch/papers/oopsla15-modelchecking.pdf
The situation seems to have gotten a bit simpler with newer versions of the nix tools (this is of no fault of the author of this post, the post is more than a year old, their blog has great haskell stuff!).
Anyway, for haskell development you can just:
1. Write cabal file (e.g., ./project.cabal)
2. cabal2nix --shell . >shell.nix
3. nix-shell
4. cabal sandbox init
5. cabal buildI did not intend to say Hoare logic being a foundation of mathematics, this was unclear in my post since I just abruptly changed topics. However, i would be delighted to read someone attempting to do just that.
What I intended to say is that the posted paper is basically a formulation of Hoare logic using set theory.
By this I meant both specifying program semantics and proving program properties. As in, the automated construction of Hoare pre/post annotations or for concurrency rely--guarantee annotations. To me, this is bringing languages without depends types closer to similar kinds of correctness guarantees.
Thanks for the clarifications on semantics. You hit the nail on the head.
However, I always found Hoare logic, and its concurrent extension Rely--Guarantee from Jones, to be quite easy to understand. The more interesting part is how to do this automatically for a user. Abstract interpretation is one way to do this, but this necessarily requires mapping some programming language to your mathematical model. However, determining the formal semantics of mature programming languages, even C, is still open research (e.g., see papers on Semantics in PLDI [3] 2015).
TLDR: verification is hard.
[1] https://en.wikipedia.org/wiki/Nicolas_Bourbaki
[2] Topoi, the categorial analysis of logic. Goldblatt, Robert. http://digital.library.cornell.edu/cgi/t/text/text-idx?c=mat...
[3] http://conf.researchr.org/track/pldi2015/pldi2015-papers#pro...
Perhaps it is because compiler messages suck but my brain has been trained to quickly pick out the line numbers and file names.
I was exposed to them in the Haskell music library Euterpea in the Haskell School of Music [2]. The signal processing API uses arrows.
[1] Generalizing Monads to Arrows. John Hughes. http://www.cse.chalmers.se/~rjmh/Papers/arrows.pdf
I'm guessing their site is designed to sell to people and not have the details.
[1] http://fbinfer.com/docs/separation-logic-and-bi-abduction.ht... [2] https://en.wikipedia.org/wiki/Coverity
Beyond that, more advanced program analysis techniques, such as model checking and abstract interpretation, use some tricky math and don't seem to be widely used outside of some niche fields (critical software).
Testing in VLSI design seems much more commonplace (people usually attribute this to the Intel bug). I don't know how much hardware design is done in a typical CS degree.
Of course if you cringe at wrapping your smoked food in foil you'll hate this way too. I'm also not sure if this is the technique he used to win his bbq medals, perhaps that's a secret.
Concurrency in Go is based on Communicating Sequential Processes (CSP) by Hoare; this was originally published in 1978. Reading CSP you see all the ideas are abstractly formalized in math terms: there really is no notion of multiple streams of execution occurring at the same time (i.e., multiple hardware threads). So, a distinction is made between things cooperating (concurrency in their parlance) and things running at the same time (parallelism).
To continue this idea, parallelism, again using their terms, really is an implementation of the more abstract concept of concurrency. That is, given a description of concurrent processes communicating you can run them in parallel (and reason about their correctness).
If you do not make the distinction, regardless of the terms you use, you remove the layers of abstraction necessary to reason about complex systems (separation of high level concepts and their implementation).
The slides call it academic but it is (barely) moving into industry. One of the, often cited, commercial uses is in one of the products coming out of Microsoft Research and into Excel, flash fill.
Another interesting application is synthesizing countermeasures for side channel attacks in crypto code [1]. They are automatically, based on the specification, guaranteed secure.
If you can find a good application, like deobfuscation, you can create some fun stuff.
> Ingredients that give the impression that they originated in a grandmother’s kitchen and have not been processed too harshly are of great appeal to consumers.
The common convenience food route minimize price and maximize flavour but ignores nutrition. They are so optimized flavor-wise that they are literally addicting. On the other hand, "natural" foods maximize "healthy sounding" ingredients. What if advancements in the food industry were used in healthy food too? For example, what if we could create a spinach salad that is as addictive as dorritos?
As an example from the article, the scientists were able to transform potato protein into something that tastes like "butter, cream, and eggs." There's no mention of the nutritional value of this stuff but imagine if it was a powder with no nutritional value (like Splenda) which you could sprinkle over your previously bland and healthy food to make it taste buttery?
Industrial processes are slowly making their way into the mainstream with books like Modernist Cuisine. As an example from the book, the common "grandmother" way to thicken gravies and other sauces is to use flour or corn starch. However, these thickeners require (1) a large amount of starch, and (2) have a large particle size. The result is that the flavour in the food decreases (perhaps now you need to add more salt), and the mouthfeel becomes gritty. Scary commercial chemicals such as N-Zorbit (Tapioca Maltodextrin) don't have this problem.
LLVM variables are sometimes called registers but they are machine independent. The bit width is arbitrary (e.g., you can create a 129-bit integer). The use of the term register is a misleading analogy; often LLVM-IR is compared to assembly language so the use of the term register was also used.
I do not know GIMPLE and couldn't find a good description of the IR instructions. But, it seems that LLVM IR is somewhat similar to low GIMPLE.
All in all, I think its sort of like a programmer learning the basics of discrete math. You're not actually learning how to program but it can change the way you think. Obviously, if you go to deep (which perhaps CSP is) you might get a bit off track.
http://c-faq.com/decl/spiral.anderson.html
(I accidentally deleted my reply)
> Computer scientists and documentation writers, take note: straight quotes and backticks in software code should never be converted to curly quotes. Those marks are, of course, part of the functional syntax of the code and must be reproduced literally. While fans of LaTeX have often written me to trumpet its typesetting superiority, I’ve never seen any LaTeX-created documentation that’s gotten this right.
As a LaTeX user (and not a very good one) I'm not too sure what I've been doing wrong.
I use Linux and I care, probably too much, about it.