The first commercially available (claimed) verified compiler

Derek Jones from The Shape of Code

Yesterday, I read a paper containing a new claim by some of those involved with CompCert (yes, they of soap powder advertising fame): “CompCert is the first commercially available optimizing compiler that is formally verified, using machine assisted mathematical proofs, to be exempt from miscompilation”.

First commercially available; really? Surely there are earlier claims of verified compilers being commercial availability. Note, I’m saying claims; bits of the CompCert compiler have involved mathematical proofs (i.e., code generation), so I’m considering earlier claims having at least the level of intellectual honesty used in some CompCert papers (a very low bar).

What does commercially available mean? The CompCert system is open source, so I guess it’s commercially available via free downloading (the paper does not define the term).

Computational Logic, Inc is the name that springs to mind, when thinking of commercial and formal verification. They were active from 1983 to 1997, and published some very interesting technical reports about their work (sadly there are gaps in the archive). One project was A Mechanically Verified Code Generator (in 1989) and their Gypsy system (a Pascal-like language+IDE) provided an environment for doing proofs of programs (I cannot find any reports online). Piton was a high-level assembler and there was a mechanically verified implementation (in 1988).

There is the Danish work on the formal specification of the code generators for their Ada compiler (while there was a formal specification of the Ada semantics in VDM, code generators tend to be much simpler beasts, i.e., a lot less work is needed in formal verification). The paper I have is: “Retargeting and rehosting the DDC Ada compiler system: A case study – the Honeywell DPS 6″ by Clemmensen, from 1986 (cannot find an online copy). This Ada compiler was used by various hardware manufacturers, so it was definitely commercially available for (lots of) money.

Are then there any earlier verified compilers with a commercial connection? There is A PRACTICAL FORMAL SEMANTIC DEFINITION AND VERIFICATION SYSTEM FOR TYPED LISP, from 1976, which has “… has proved a number of interesting, non-trivial theorems including the total correctness of an algorithm which sorts by successive merging, the total correctness of the McCarthy-Painter compiler for expressions, …” (which sounds like a code generator, or part of one, to me).

Francis Morris’s thesis, from 1972, proves the correctness of compilers for three languages (each language contained a single feature) and discusses how these features may be combined into a more “realistic” language. No mention of commercial availability, but I cannot see the demand being that great.

The definition of PL/1 was written in VDM, a formal language. PL/1 is a huge language and there were lots of subsets. Were there any claims of formal verification of a subset compiler for PL/1? I have had little contact with the PL/1 world, so am not in a good position to know. Anybody?

Over to you dear reader. Are there any earlier claims of verified compilers and commercial availability?

Deep Tech is affecting people’s lives without them even knowing it.

Paul Grenyer from Paul Grenyer


Deep Tech sounds like a character from the X-Files right? While it’s not a covert government agency, Deep Tech is affecting people’s lives without them even knowing it, but it’s not something we need to be afraid of. There are lots of very technical and wordy definitions of Deep Tech, but essentially it means technology that has an engineering aspect while having a demonstrable impact on people’s daily lives. Rather than a disruptive technology, like AirBnB or Deliveroo – apps that alter a service that already existed – a Deep Tech breakthrough could use technology to cure cancer or expand space travel. AirBnB is an intangible app, while Deep Tech often involves robots or breakthroughs in scientific or medical equipment.

Good examples are artificial wombs to increase the survival chances of premature babies, or brain implants to improve the independence of stroke victims. It’s not just medical advancements that are benefitting from Deep Tech, but improvements to smart homes and cleaner cities as well as energy efficiency are all developing areas of Deep Tech. Self driving cars and lithium-ion batteries could vastly improve the environment and how we live in it and are both examples of Deep Tech. Since

2015 European investment in Deep Tech has been growing three times faster than B2C investments (Wavestone) and it’s easy to see why when the impact that technology of this kind can have is made clear. Rather than just making it easier for people to order the weekly shop, or interact with a video on social media, discoveries in the Deep Tech arena make fundamental changes to how we live and survive. Researchers and scientists working in Deep Tech have not only created machines that can replicate human actions, but improve them. Like something from a science fiction movie, ‘HoloEyes’ are goggles that can provide a surgeon with a patient’s anatomy before the first incision is made, right there in the operating room. Harvard scientists have gone one further into the science fiction realm and created a brand new material, never before seen on earth. Metallic hydrogen was formed after 45 years of research and tests and has enormous potential, from space travel to superconducting abilities.

Deep Tech is technology at its most advanced and it’s most useful. While it may not affect all of us at once, the advancements being made in this field have a huge impact that will influence and hopefully improve daily life on a global scale.

Talk to me about Deep Tech.

Always Reply Within Your SLA – Succeed or Abort

Chris Oldwood from The OldWood Thing

Way back in 2012 I wrote the blog post “Service Providers Are Interested In Your Timeouts Too” about how you can help service teams understand your intentions so that they can handle requests more efficiently. That was written at a time when I had been working for many years on internal systems where there were no real SLAs per-se, often just a “best efforts” approach with manual intervention required to “unblock” the system when the failures start occurring [1]. In contrast I have always strived to create self-healing systems as much as possible so that only truly remarkable events require any kind of human remediation.

In more recent years I’ve spent far more time working on web services where there is a much stronger notion of an SLA and therefore a much higher probability that if you fail to meet your SLA then the client will attempt to perform some kind of recovery rather than hang around and wait for the reply [2]. Hence what I wrote about wasting resources on dead requests in that earlier blog post have started to become more significant.

Deadlines

A consequence of this ideology is that I’ve started to become far more interested in the approach of always responding within the SLA even if that means aborting mid-request. Often an SLA is seen as an aspiration rather than any kind of hard deadline, something which we hope to achieve more often than not, where “more often” usually involves quoting some (arbitrary) number of “nines”. For those requests that fall outside this magical number all bets are off and you might get an answer in a useful timeframe or you might not. This kind of uncertainty has always bothered me as a client consumer.

Hence, I’ve started moving towards building services that always provide a reply within the SLA whether or not the request has been satisfied. Instead of tying up valuable resources in the hope that when the answer finally arrives the client still has a vested interest in it, I’d prefer to just abandon the request and let the client know the SLA would be violated if it had continued servicing it. In essence the request times-out server-side, where the time-out is the SLA.

What this means for the client is that they have a definitive reply (network issues notwithstanding) to their request within the time limit allowed. More importantly if they want to allow more time to handle the request than the SLA allows for then they need to tell the service that they’re willing to wait. Essentially this creates a priority system and allows the service to decide what to do with requests that are happy to hang around for a bit longer.

Mechanics

Implementation-wise what this mostly boils down to is ensuring that every non-trivial piece of work (think: database query, network call, disk read, etc.) must be made with a bounded call time, i.e. one where a timeout can be provided so that the caller always regains control in a timely fashion. Similarly we don’t start any work that we suspect we can’t finish in time either. This generally manifests as aborting on the first timeout which is usually given the entire SLA and therefore you’re never going to recover in time.

Internally the maximum timeout starts with the SLA and as each background query is sent it is timed and the timeout gets progressively shorter [3]. As the load increases and internal queries take longer the chances of a request aborting rises but at least the load on the upstream systems doesn’t keep rising too. Ultimately it’s just a classic negative feedback loop.

Limitations

Unfortunately what makes implementing this somewhat less than idea is that we still don’t really have cancellable requests in many frameworks and you’re never entirely sure what happens when the timeout triggers. If the underlying operation is abandoned, but has to complete anyway because it can’t be cancelled, you may not be much better off. The modern async-enhanced programming world is great for avoiding tying up threads in the happy path but once you start considering the failure modes it’s much harder to reason about and, more importantly, control what’s going to happen. Despite the fact that under the covers the world of I/O has practically always been asynchronous the higher layers still assume a synchronous model with syntactic sugar only helping to reinforce that perspective.

So far I don’t have nearly enough production-level data points to know if it’s an idea that is truly worth the effort to implement or not. Being able to reject work outright because you’ve already missed the SLA isn’t too onerous but does mean you need to tap into the processing pipeline early before the request is queued in the background to know when the internal clock has started ticking. What’s harder to determine is whether you really get any benefit out of the additional complexity needed to track your request’s progress and if aborting upstream requests creates a more or equally unstable service due to the way the timeouts leave their underlying requests dangling.

I still think it’s an approach worth pursuing but I wouldn’t be surprised to find The Morning Paper covering something from decades ago that shows it’s just a fools errand :o).

 

[1] See “Support-Friendly Tooling” for some other examples about how this can play out if reliability out-of-the-box is “assumed”.

[2] In one instance that would mean abandoning the request and potentially taking on some small financial risk on behalf of the customer.

[3] Naturally for parallel / scatter-gather I/O it’s the time of the longest concurrent request.

Publishing information on project progress: will it impact delivery?

Derek Jones from The Shape of Code

Numbers for delivery date and cost estimates, for a software project, depend on who you ask (the same is probably true for other kinds of projects). The people actually doing the work are likely to have the most accurate information, but their estimates can still be wildly optimistic. The managers of the people doing the work have to plan (i.e., make worst/best case estimates) and deal with people outside the team (i.e., sell the project to those paying for it); planning requires knowledge of where things are and where they need to be, while selling requires being flexible with numbers.

A few weeks ago I was at a hackathon organized by the people behind the Project Data and Analytics meetup. The organizers (Martin Paver & co.) had obtained some very interesting project related data sets. I worked on the Australian ICT dashboard data.

The Australian ICT dashboard data was courtesy of the Queensland state government, which has a publicly available dashboard listing digital project expenditure; the Victorian state government also has a dashboard listing ICT expenditure. James Smith has been collecting this data on a monthly basis.

What information might meaningfully be extracted from monthly estimates of project delivery dates and costs?

If you were running one of these projects, and had to provide monthly figures, what strategy would you use to select the numbers? Obviously keep quiet about internal changes for as long as possible (today’s reduction can be used to offset a later increase, or vice versa). If the client requests changes which impact date/cost, then obviously update the numbers immediately; the answer to the question about why the numbers changed is that, “we are responding to client requests” (i.e., we would otherwise still be on track to meet the original end-points).

What is the intended purpose of publishing this information? Is it simply a case of the public getting fed up with overruns, with publishing monthly numbers is seen as a solution?

What impact could monthly publication have? Will clients think twice before requesting an enhancement, fearing public push back? Will companies doing the work make more reliable estimates, or work harder?

Project delivery dates/costs change because new functionality/work-to-do is discovered, because the appropriate staff could not be hired and other assorted unknown knowns and unknowns.

Who is looking at this data (apart from half a dozen people at a hackathon on the other side of the world)?

Data on specific projects can only be interpreted in the context of that project. There is some interesting research to be done on the impact of public availability on client and vendor reporting behavior.

Will publication have an impact on performance? One way to get some idea is to run an A/B experiment. Some projects have their data made public, others don’t. Wait a few years, and compare project performance for the two publication regimes.

Statistical techniques not needed to analyze software engineering data

Derek Jones from The Shape of Code

One of the methods I used to try to work out what statistical techniques were likely to be useful to software developers, was to try to apply techniques that were useful in other areas. Of course, applying techniques requires the appropriate data to apply them to.

Extreme value statistics are used to spot patterns in rare events, e.g., frequency of rivers over spilling their banks and causing extensive flooding. I have tried and failed to find any data where Extreme value theory might be applicable. There probably is some such data, somewhere.

The fact that I have spent a lot of time looking for data and failed to find particular kinds of data, suggests that occurrences are rare. If data needing a particular kind of analysis technique is rare, there is no point including a discussion of the technique in a book aimed at providing general coverage of material.

I have spent some time looking for data drawn from a zero-inflated Poisson distribution. Readers are unlikely to have ever heard of this and might well ask why I would be interested in such an obscure distribution. Well, zero-truncated Poisson distributions crop up regularly (the Poisson distribution applies to count data that starts at zero, when count data starts at one the zeroes are said to be truncated and the Poisson distribution has to be offset to adjust for this). There is a certain symmetry to zero-truncated/inflated (although the mathematics involved is completely different), plus there is probably a sunk cost effect (i.e., I have spent time learning about them, I am going to find the data).

I spotted a plot in a paper investigating record data structure usage in Racket, that looked like it might be well fitted by a zero-inflated Poisson distribution. Tobias Pape kindly sent me the data (number of record data structures having a given size), which I then failed miserably to fit to any kind of Poisson related distribution; see plot below; data points along red line through the plus symbols (code+data):

Number of Racket record data structures having a given size.

I can only imagine what the authors thought of my reason for wanting the data (I made data requests to a few other researchers for similar reasons; and again I failed to fit the desired distribution).

I had expected to make more use of time series analysis; but, it has just not been that applicable.

Machine learning is useful for publishing papers, but understanding what is going on is the subject of my book, not building black boxes to make predictions.

It is possible that researchers are not publishing work relating to data that requires statistical techniques I have not used, because they don’t know how to analyze the data or the data is too hard to collect. Inability to use the correct techniques to analyze data is rarely a reason for not publishing a paper. Data being too hard to collect is very believable, as-is the data rarely occurring in software engineering related work.

There are statistical tests I have intentionally ignored, the Mann–Whitney U test (aka, the Wilcoxon rank-sum test) and the t-test probably being the most well-known. These tests became obsolete once computers became generally available. If you are ever stuck on a desert island without a computer, these are the statistical tests you will have to use.

Visual Lint 6.5.5.300 has been released

Products, the Universe and Everything from Products, the Universe and Everything

This is a recommended maintenance update for Visual Lint 6.0 and 6.5. The following changes are included:
  • Fixed an MSBuild parsing bug which was preventing Visual Studio system include folders from being read in some circumstances.
  • Fixed a bug which could prevent the VisualLintGui code editor determining the location of PC-lint Plus indirect files in order to open them from a context menu.
  • Updated the values of _MSC_VER and _MSC_FULL_VER in the PC-lint Plus indirect file co-rb-vs2017.lnt for compatibility with Visual Studio 2017 v15.8.3. This change is needed to fix a fatal error in yvals_core.h if _MSC_VER is less than 1915.
  • Added a PC-lint Plus compatible version of lib-stl.lnt to the installer as it is not currently supplied with PC-lint Plus.
  • Added additional indirect files needed for analysing Visual Studio 2012, 2013 and 2015 codebases with PC-lint Plus 1.2 to the installer.
  • If a project intermediate files folder does not currently exist, it will not be referenced with a -i (include folder) directive on generated PC-lint or PC-lint Plus command lines. This avoids extraneous 686 warnings "(Warning -- option '-i' is suspicious: absolute path is not accessible)".

    Note that if build artifacts (e.g. .tlh or .tli files) are required for analysis purposes, analysing without the intermediate folder will most likely result in analysis errors. In this case, performing a build and re-analysing the affected files/projects should fix it.
Download Visual Lint 6.5.5.300

More Continuous #NoProjects questions

Allan Kelly from Allan Kelly Associates

QA-2018-10-24-14-20.jpg

Three short questions and answers to finish off my series of left over questions about #NoProjects, #NoEstimates and the Continuous model.

Q4: How do we prioritize and organize requests on a product that are from opposite business owners? – for example legal (who wants to reduce the risk and annoy more customers) and sales (who want to increase the features and simplify life) can be arbitrated in a backlog?

You can think of this as “which is worth more apples or milk?” It is difficult to compare two things which are actually different. Yes they are both work requests – or fruit – and each can make a case but at the end of the day you can’t make everything number 1 priority.

In real life we solve this problem with money.

Walk into your local supermarket. Apples, oranges and milk are both price in the same currency, sterling for me, Francs for the person who asked this question, maybe Euro’s or Dollars for you. So if we can assign value points to each request we are half way to solving the problem.

Now sales will argue that without their request there is no real money so whatever they ask for is worth more. And legal will argue that nobody wants to go to jail so their request must be worth more. You can set your analyst to work to calculate a value but a) this will take time and b) even when they have an answer people will dispute it.

Therefore, I would estimate a value – planning poker style. With an estimates value there is no pretence of “right” or “correct”. Each party gives a position and a discussion follows. With luck the different sides converge, if they don’t then I average. Once all requests are valued you have a first cut at prioritisation.

Q5: How to evaluate the number of people you need to maintain software?

I don’t. This is a strategic decision.

Sure someone somewhere needs to decide how much capacity – often expressed as people – will be allocated to a particular activity but rather than base this on need I see this as another priority decision. If a piece of software is important to an organization then it deserves more maintenance, and if it is not important it deserves less.

You could look at the size of the backlog, or the rate of new requests and contrast this with the rate at which work gets done. This would allow you to come up with an estimate of how many people are needed to support a product. But where is the consideration of value?

Instead you say something like: “This product is a key part of our business but the days of big changes are gone. Therefore one person will be assigned to look after the software.”

If in three months more people in the business are demanding more changes to the software and you can see opportunities to extract more value – however you define value – then that decision might be revised. Maybe a second person is assigned.

Or maybe you decide that maintaining this product isn’t delivering more value so why bother? Reduce work to only that needed to keep it going.

Q6: How do you evaluate the fact that your application becomes twice as fast (or slower) when you add a new feature in a short period of time?

Answering this question requires that the team has a clearly defined idea of what value is. Does the organization value execution speed? Does the organization value up-time? Does the organization value capacity?

Hopefully some of this will have come out of the value estimation exercise in Q4, if not the analysis is just going to take a bit longer. The thing to remember is: what does the change do for the business/customers/clients? Being faster is no use in itself, but doing X faster can be valuable.

The real problem here is time. Some changes lead to improvements which can be instantly measured. But there are plenty of changes where the improvements take time to show benefit. Here you might need to rely on qualitative feedback in the short run (“Sam says it is easier to use because it is faster”). Still I would keep trying to evaluate what happens and see if you can make some quantitive assessment later.

Notice that Q4 and Q6 are closely related. If you have a clear understanding of why you are doing something (Q4) then it becomes easier to tell if you have delivered the expected value (Q6). And in trying to understand what value you have delivered then you refine your thinking about the value you might deliver with future work.

Another feedback cycle.


These questions concludes the series of question carried over from the #NoEstimates/#NoProjects workshop in Zurich – see also How should we organize our teams?Dealing with unplanned but urgent workHow do we organise with a parallel team? – if you would like me to answer your question in this blog then please just e-mail me.


The #NoProjects books Project Myopia and Continuous Digital discuss these and similar issues in depth and are both available to buy in electronic or physical form from Amazon.

CDMyopia-2018-10-24-14-20.jpg

The post More Continuous #NoProjects questions appeared first on Allan Kelly Associates.

LintProject Pro End of Life Notice

Products, the Universe and Everything from Products, the Universe and Everything

LintProject Pro is a command line only product which can perform a basic per-file analysis of a C/C++ codebase using PC-lint or CppCheck. In many ways it was the proof of concept for Visual Lint, and although it has served us well, it's getting a bit long in the tooth now. For example, unlike Visual Lint Build Server Edition (which inherited its capabilities), LintProject Pro doesn't support PC-lint Plus and only makes use of a single CPU core when running analysis. The interfaces to the two products are however very similar as the command line interface of Visual Lint Build Server is based on that of LintProject Pro. In fact, Visual Lint Build Server Edition can do everything LintProject Pro can - along with much, much more. As such we think it is now finally time to put LintProject Pro out to pasture, and to make that easier we are offering a migration path from LintProject Pro to Visual Lint Build Server Edition. This involves trading in each existing LintProject Pro licence puchased before 23rd October 2018 for a 25% discount on a corresponding Visual Lint Build Server Edition licence. As such LintProject Pro will be removed from our online store very soon. To take advantage of the upgrade, just write to us quoting which LintProject Pro licence (or licences) you wish to trade-in. We've tried to keep this process clear and simple. The value of the discount offered exceeds that of the LintProject Pro licence, so this is a lower cost route to obtain an equivalent PC-lint Plus compatible product than (for example) refunding any existing LintProject Pro licences and purchasing Visual Lint Build Server Edition licences at full price. If you have any questions, just ask.

The Art of Prolog – reading another classic programming text

Timo Geusch from The Lone C++ Coder's Blog

I did have to learn some Prolog when I was studying CS and back then it was one of those “why do we have to learn this when everybody is programming in C or Turbo Pascal” (yes, I’m old). For some strange reason things clicked for me quicker with Prolog than Lisp, which I now […]

The post The Art of Prolog – reading another classic programming text appeared first on The Lone C++ Coder's Blog.