Experimenting with CompCert

A few weeks ago I experimented with CompCert, a C compiler from INRIA, written largely in Coq, with chunks in OCaml; this allows the Coq parts of CompCert to be formally verified (see below for more on this).

Now I have no need of a guarantee that my compiler is bug-free, but to the extent that translation my code into the subset of C supported by CompCert reduces the bugcount rather than increases it, it’s a win. I’m basically using compcert as a lint tool, but it’s fun and instructive anyway. The real-world scenario which makes any of this interesting is therefore if you have a C codebase and suspect a bug in your compiler and want to know how hard it would be to maintain that codebase such that it compiled with a compiler believed to be bug free.

For many years I have maintained a codebase of 40K lines of fairly odd C, that implements a computer game I used to run in the 1990s, and which predates modern conveniences that might have been used, such as sqlite, pcre, libevent, reliable IP stacks on NeXTSTEP, ANSI C, free C++ compilers, free Erlang, etc, etc. The code is also unusual in shunning the use of struct, malloc and pointer arithmetic. For almost the last twenty years I’ve kept it up-to-date with the C toolchains on a number of OSes, as a way of keeping an eye on what the cool kids are breaking.

So:

Firstly, the codebase needs to be able to cope with multiple compilers; gcc and LLVM’s clang are close to drop-in replacements for each other from the perspective of the Makefile. Not so, CompCert: -Wall -Werror are not accepted as options by CompCert, as they’re effectively on by default. CompCert isn’t going to want to know about any code that doesn’t pass gcc -Wall -Werror, but there are a few things LLVM thinks it’s Ok to warn you about that CompCert is cool with, which feels like LLVM is wasting my time. Getting the build system and revision control happy about parameterisable compiler options has to happen first.

I was forced to do change all the remaining instances of conflation of integer widths. Anyone who’s done arithmetic in OCaml will recognised this as one of the house microfascisms of INRIA, but it’s a deep issue: a lot of corner cases depend on your installation of the header files and libraries and so on. In my case, function prototypes are culled into a .h file automatically with cproto, which by default changes the width of integers in K&R-style C functions:

void my_function(i)
short i
{
    ...
}

is output as

void my_function(int i);

which gcc and LLVM tolerate, but CompCert doesn’t. There were a couple of other legitimate “Well Don’t Do That Then” moments that I won’t tax you with. Effectively one’s forced to get all the prototypes and headers and includes exactly right. This showed up a bug: a variable which was supposed to be declared extern wasn’t, and was separately allocated from the global it was supposed to represent.

The more formal treatment of integer widths also meant fixing a lot of sprintf format strings.

The next thing I had to fix was the idiom

    char *messages[] = { "...", "...", "...", NULL };
    int x = sizeof(messages) / ...;

CompCert insists on the length of messsages[] being explicitly specified, which means this technique isn’t allowed.

The harder stuff was signal() and stdarg; basically, CompCert supports an anaemic subset of C, and doesn’t allow stdargs, though it provides the sprintf() clique of functions. Since wrapping sprintf() is about the only thing varargs is used for in C, this turns out not to be a problem, but I originally bet that parts of the codebase were outside the CompCert C dialect and would need to be shunted into libraries.

My own adventure in CompCert land basically amounted to learning new stylistic restrictions in C. Reading around what people have been doing with CompCert I came across a few interesting articles and from this chap I learnt about concolic testing which is another technique I have no use for but am glad to have spent time learning about.

If you could bear reading this far, you should follow me on Twitter:

An independent Scotland will be outside the European Union

If the people of Scotland vote to leave the United Kingdom this week, customs checks along the new border are practically unavoidable. Alex Salmond claims that Scotland will continue to be part of the EU. He’s bluffing, and without membership of Europe’s Customs Union, his newly independent country will no longer be able to export goods to England tariff-free: anything crossing the border must be examined and taxed, and a cut sent off to Brussels.

It’s perfectly possible for Scotland to rejoin the EU after 2016, and the difficulty of doing so is being exaggerated by unionists, but automatic membership is legally impossible. The members of the European Union are states, not peoples or territories, and to gain membership a state must be approved by the governments of all the other EU member states.

Except in France.

Under Article 88-5 of the French constitution, the French Government no longer has the power to approve new EU member states by itself. The political elite there is so distrusted that new states must be approved by the people in a referendum, or by a supermajority in Parliament. Has Mr Salmond made a secret deal with the French people, or perhaps with the rightwingers and nationalists of the French opposition, or is he just winging it again? The French are not going to ignore their own constitution to help the SNP, as letting the French political class admit new countries to the EU means letting Turkey into the EU, and that is about as popular in France as cutting agricultural subsidies, so somehow the politicians or the people need to be bargained with.

Even if Salmond said he hadn’t made a secret deal with any foreign rightwinger other than Rupert Murdoch, we should not believe him: his administration spent thousands of pounds of taxpayer’s money trying to prevent the disclosure of legal advice on Scotland’s EU membership when in fact this advice didn’t exist in the first place. Would you believe non-existent advice from this man?

For an indpendent Scotland to rejoin the EU, it needs to conclude a treaty with the existing member states, including the rump UK. This can’t be done while Scotland is still part of the UK (particularly from the perspective of the French constitutional requirements). This means months or years of disrupted cross-border trade and customs checks along the Tweed, at Euston Station and so on while the other countries sign up.

Much has been made of the potential attitude of governments in Spain, Cyprus, Greece and other places with sensitivities about secessionism. Particularly troublesome are countries such as Spain and Cyprus which have territorial claims against the UK in Gibraltar and Akrotiri. Foreign politicians can demand that the UK abandon naval and military bases in the Mediterranean as the price for restoring customs-free trade in Great Britain. This is not a situation David Cameron should have allowed to come into existence. The Scottish Government has spent taxpayer’s money brushing off Freedom of Information requests asking what discussions they have had with Spain and Cyprus over this issue. Maybe those discussions didn’t happen either!

Scotland may well be better off outside the EU; after all, small non-EU states like Norway and New Zealand do fine, but pretending that the country won’t spend a day outside the EU is insulting to Scottish voters and the nation as a whole.

If you could bear reading this far, you should follow me on Twitter:

Istos custodes

Ofsted is now in a dispute with the Department for Education about no-notice inspections. Puzzled readers may wonder why any school inspection involves notice, for to give notice transforms the inspection regime from an enforcement mechanism to a protection racket: you can run schools however you want, but only if you’re organised enough to cover it up between notification of an inspection and clipboard hitting the desk two days later.

If you could bear reading this far, you should follow me on Twitter:

Instrumentalising the criminal law, part 94

Sometimes the public sector unions ask for the criminal law to be changed to make it a more serious offence to assault public servants; there was an apparently unsuccessful attempt a decade ago.

I wonder whether they think these laws should apply to union members who assault scabs and strike breakers during industrial disputes.

If you could bear reading this far, you should follow me on Twitter:

Not muddying the waters about Euroscepticism

The author of this Kosmopolit article makes the claim that it’s silly to label people or arguments using the terms “Europhile” and “Eurosceptic”.

That’s just wrong; the terms work perfectly fine, they describe whether someone favours the EU vis-a-vis the member states (or similar actors). If you want your country to leave the EU, you’re a Eurosceptic. If you want to repatriate powers, you’re a Eurosceptic. If you oppose the transfer or arrogation of new powers to the EU, you’re a Eurosceptic. The converse positions make you a Europhile.

Where it gets interesting (and in the Kosmopolit article, this is where the straw-man style argumentation and rhetorical questions all start to appear) is in two areas: internal conflicts between EU institutions, and situations where the EU does things that particular Eurosceptics support.

Eurosceptics are just not going to agree with each otherabout intra-institutional conflicts between Council, Court, Commission and Parliament. Why should they? It’s like asking people who favour labour against capital which side they back in a dispute between shareholders, board and management: their ideology just doesn’t discriminate at that level of detail, though individuals might have opinions on a general or case by case basis. It’s a matter of strategy and tactics, not an issue of principle.

Similarly, there will be cases where Eurosceptics are divided about particular EU policies, such as the Euro, surveillance, IP laws, etc. Ignoring the people who tactically support bad policies in the hope of hastening the EU’s demise, there’s no reason that people who want less EU power are going to agree on any other issue: Tony Benn, Margaret Thatcher, Enoch Powell, Michael Foot, Bob Crow, Nigel Farage, Dan Hannan, Dennis Healey, David Owen, and Kate Hoey are all over the political “spectrum”. It’s inevitable that the EU will often do things that some of them support. One principled view is to say that one opposes all exercises of competences that the EU should not have, and this is completely normal in the United States: Republican opponents of gay marriage nevertheless oppose federal bans on gay marriage on states rights’ grounds.

Once one has taken into account such positions, the Kosmopolit argument isn’t very convincing. He/she says “So just because I think the policy outcome is positive I am considered a “europhile”?”. A Question To Which The Answer Is No.

If you could bear reading this far, you should follow me on Twitter:

Other things Churchill liked

We’re often reminded that Churchill supported the ECHR or European integration more broadly, as though there were no better argument in favour or against these things.

For a bit of perspective, here’s a broader list of stuff Churchill liked:

  • “using poisoned gas against uncivilised tribes”
  • the Gold Standard
  • denying India’s right to be independent
  • using the army against strikers
  • politicians issuing orders to the police
  • the European Convention on Human Rights
  • European integration
  • imperialism more generally
These people need some better arguments, or at least to explain why their cause gets to be associated with Churchill’s admirable qualities rather than his flaws.

If you could bear reading this far, you should follow me on Twitter:

The Day We Fight What Exactly?

It’s no longer safe in the UK to talk to your GP about depression and mental illness – the government will force them to hand over this information, whereupon it may be leaked, hacked, sold, etc.

If you could bear reading this far, you should follow me on Twitter:

Aliens don’t crash land

Today is the anniversary of the Roswell Incident, which is the subject of various conspiracy theories. I don’t like conspiracy theories; that way of thinking always tends to involve being selective about whether particular things are plausible.

There’s no reason to suppose that life necessarily exists outside our solar system, or that it is impossible for life to exist elsewhere, but that is not the point: we are invited to believe that intelligent creatures from outside our solar system crash landed in Roswell this day sixty-six years ago.

Is plausible that aliens could master interstellar travel, but not the ability to land without crashing?

If you could bear reading this far, you should follow me on Twitter:

The stakes of the EU debate just got a lot lower

We’re often told that the particular form of European integration we currently endure is somehow necessary for preventing another war in Europe.

Since Croatia’s accession last night, the cost of the most recent war in which EU member states were on opposite sides has now collapsed. Twenty-two years ago this week, Slovenia and Croatia fought on opposite sides of the Ten Day War which secured the former’s independence from Yugoslavia; no-one really wanted to be fighting, and the unhappy state of affairs constituted one of the least violent wars of all time: only 63 people were killed.

That magnitude of loss and foreshortening of human life is at the sort of scale that pharmaceutical regulators have to deal with when licensing drugs for use in the health system. In a world of finite resources and finite altruism, someone has to choose what drugs and medical procedures should be available at the expense of the taxpayer, and that means weighing the lives and health of different groups of people: if you have the cash to help either the diabetic or the woman with breast cancer, but not both, you have to have a reason for placing the life of one above the other. Just flipping a coin is morally repugnant. This is why we have QALYs.

A regulatory decision which makes drugs more expensive costs lives and suffering. Every time the EU’s deliberately undemocratic processes are captured by rent-seeking lobbyists trying to increase medical patent protection, there is a cost measurable in QALYs. Now when politicians raise the spectre of war to silence critics, those critics can say “well, the last war only cost 20000 QALYs, and your proposal looks worse”.

If you could bear reading this far, you should follow me on Twitter:

National Parliaments and EU Legitimacy

Jon Worth, Charles Grant and Ralf Grahn have been writing about the various options for giving national parliaments a role in the EU’s legislative process. This conversation between people who fundamentally agree that the EU in some form is desirable involves so many mistaken assumptions and false assertions that it’s impossible to deal with them all in a blog post of bearable length.

One feels like one’s wasting one’s breath even (re)stating all this but:

  • the EU won’t be legitimate until the people consent to its exercise of its current competences; what it will take to convince me that the requisite consent is present is a matrix showing, for every country C and subject S, that opinion polls say that the generality of people in county C are happy for their country to be bound by an EU-wide majority when laws are made about subject S; that’s how it works in real democratic federations
  • the “red card” proposals for national parliaments to have some role in blocking legislation only apply when the legislation violates the so-called principles of subsidiarity or proportionality, not when the legislation is outside the competence of the EU entirely
  • the EU does not have a demos, despite Mr Grahn’s reference to Miss Melchior’s assertion to the contrary. No test is suggested by either of them for how one might verify that the EU has a demos
  • vesting any sort of veto or consultative power in national parliaments is not going to improve input legitimacy
  • the best way to improve legitimacy is not to focus on outputs; there can be no such thing as a benevolent dictatorship, in theory or in practice; the exhaustive work of Bruce Bueno de Mesquita completely demolishes the case that it’s possible to improve citizens’ wellbeing whilst maintaining a kleptocracy
  • the democratic deficit is not a perception, it is a reality, and Mr Grant should concentrate on the wellbeing of actual voters rather than the opinions of the Quislington dinner party conversationalists to whom he seems to regard himself as exclusively accountable
  • unless “do you agree to be part of this country” is counted as part of “input legitimacy”, then the two-way split between input legitimacy and output legitimacy fails to capture a fundamental aspect of real political legitimacy. People in Ireland in 1918 and today in Northern Ireland rejected government from Westminster over any and all subjects; it was never the complaint that UK government was undemocratic, and if the EU were a democracy, many countries (more!) would still not want to be part of it
More seriously, adding national parliaments just adds more veto players; the problem is that people in individual countries don’t see it as in their interests to be bound by an EU-wide majority on almost any issue. The EU has already effectively arrogated to itself the power to legislate on any issue, but cannot get this ratified by the people, either incrementally or all at once.

If you could bear reading this far, you should follow me on Twitter: