buttproblem

I'm curious about how you use this during debugging, would you mind elaborating on what language(s) you're using the call-graph from?

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.

Techniques like this can be used to make debugging better. There's a lot of work towards this direction but there are some difficulties making it's use widespread.

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.

Overall, one way to look at formal methods is that the tools range from fully automated (e.g., abstract interpretation, model checking), to manual (e.g., interactive theorem proving). Along this same range, the complexity of properties which can be proved also moves from simple (e.g., absence of buffer overflows) to complex (termination of parameterized systems).

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/

[3] http://www.astree.ens.fr/

[4] https://klee.github.io/

[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

[9] http://plrg.eecs.uci.edu/software_page/42-2/

I was just trying to get Nix working after needing a version of base (GHC) newer than what I had installed.

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

After step 3, all the required packages, including stuff like GHC, will be installed. You can use cabal however you normally do to build the project:

   4. cabal sandbox init
   5. cabal build

Thanks for the interesting history on set theory. However, if you read [1] or the first chapter of [2] in my reply you'll see that the strides to formalize mathematics started in 1935 so something does not add up.

I 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.

At least since 1935 [1, 2] people have been trying to formalize all of mathematics with set theory. I always thought this was fairly interesting, similar to how the real numbers can be modeled in a language using dependent types like Coq.

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...

I agree both in parsing via another program as well as parsing error messages in my brain (not sure which you were intending).

Perhaps it is because compiler messages suck but my brain has been trained to quickly pick out the line numbers and file names.

I don't know node, but, conceptually, Arrows [1] map to the steam concept very well (as always in Haskell, they are more general). The sugar in Haskell to use them similar to do-notion is really a joy to use.

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

[2] http://haskell.cs.yale.edu/?post_type=publication&p=112

I'd be interested in this as well; all I could find on their site is that it is uses "patened techniques." Considering the first seperation logic paper was published in 2001 [1] and Coverity founded in 2002 [2], they probably did not (at least originally) use the same techniques.

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

testing seems to be somewhat of a niche field. Using manual unit testing and random testing gets good results and seems to be the standard. But, you certainly could not devote an entire semester course on them.

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.

Nathan Myhrvold in Modernist Cusine writes about a similar technique. Sous vide first, followed by a brief time in the oven, and finished on a smoker. This seems to be the reverse of the crutch. (The oven is used to prime the meat for smoking and is apparently based on a German technique for making sausages.)

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.

While I agree with you, it is better to focus on practical things other than pedantic names, you can really notice the difference more when you look at the foundation of Go's language level concurrency paradigm.

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).

There's a lot of work going on in this field; if it were really scalable it would be awesome.

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.

[1] http://www.ece.vt.edu/chaowang/pubDOC/EldibW14CAV.pdf

The author of this article and the food industry seem to know what the people want:

> 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 doesn't have an intermediate representation comparable to Gimple: LLIR seems to be at the level of the registers rather than the nice abstract Gimple

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.

While I am curious too about your question, Vapnik was previously working in industry at NEC Labs in New Jersey.

One way of testing/verifying concurrent programs is to build a model of the program, and then see if the model satisfies certain properties. This is fairly tedious and does not scale very well. However, while it wont prove anything, it can be useful to build some kind of model; it can often point out some flaws in the design that you missed.

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.

The most useful education I got on reading function pointers is the spiral rule:

http://c-faq.com/decl/spiral.anderson.html

(I accidentally deleted my reply)

I wonder if someone could shed some light on this (from type composition straight and curly quotes):

> Computer sci­en­tists and doc­u­men­ta­tion writ­ers, take note: straight quotes and back­ticks in soft­ware code should nev­er be con­vert­ed to curly quotes. Those marks are, of course, part of the func­tion­al syn­tax of the code and must be re­pro­duced lit­er­al­ly. While fans of LaTeX have of­ten writ­ten me to trum­pet its type­set­ting su­pe­ri­or­i­ty, I’ve nev­er seen any LaTeX-cre­at­ed doc­u­men­ta­tion that’s got­ten this right.

As a LaTeX user (and not a very good one) I'm not too sure what I've been doing wrong.

I see how this is interesting but I can't get over how the author says, "When contrasting this with Eric's video", but "Eric's video" is a different program than the novice programmer. Maybe this is me being too pedantic.

> I think if users _have_ to have something different they will seriously consider OSX and Linux. One is more polished on better hardware for people who have money and want the best. The other is free for people who don't care.

I use Linux and I care, probably too much, about it.