How programmers make sure that their software is correct
lemire.me
lemire.me
Bugs caused by misunderstood or unexpected interactions between subsystems and specification bugs seem to predominate these days IME but discussion about sophisticated ways of dealing with these things seems fairly scant.
I, the same developer, spent a good hour recently trying to iron out the bugs in a piece of code that concatenated two integers bit-wise and calculated the offset point. That is, given two integers whose bits are
00000000,00000000,00000000,0PPPPPPP
00000000,000000QQ,QQQQQQQQ,QQQQQQQQ
The code should produce the shortest an array of bytes that looked like ZZZZZZZZ,0000000P,PPPPPPQQ,QQQQQQQQ,QQQQQQQQ
Where Z in this case would be 18, the offset of P's bits. This is finicky in a way I've never encountered while I worked in finance. It's not exorbitantly difficult, but there are just a lot of potential logic errors to make.The code, ultimately, looked like this (it's Java hence the extra awkward bit twiddling)
int pw = bitWidth(p);
int qw = bitWidth(q);
int pwr = (pw%8);
int totalSize = (pw + qw)/8 + (((pw+qw)%8)>0?1:0);
byte[] data = new byte[totalSize + 1];
int b = data.length - 1;
while (p > 0) {
data[b]=(byte)(p&0xFF);
p = p >>> 8;
if (p != 0) {
b--;
}
}
if (pwr != 0) {
while (q > 0) {
data[b--] |= ((byte) ((q << (pwr)) & 0xFF));
q = q >>> (8-pwr);
data[b] |= (byte) (q & 0xFF);
q = q >>> pwr;
}
}
else {
while (q > 0) {
data[--b] |= (byte)(q&0xFF);
q = q >>> 8;
}
}
data[0] = (byte) pw;
return data;
It's like 40 lines of code. It shouldn't be that hard. Yet it is. Bit-twiddling is error prone and hard to reason about and, dunno, maybe pwr isn't a great variable name, but the code really doesn't get particularly expressive even if you change it to pWidthRemainder or whatever. It's still basically a bunch of cthulhu fhtagn as far as I'm concerned.The lexicon supports several billion entries entirely in memory, which requires a lot these eldritch coding tricks (since Java certainly wasn't built for that many objects, GC and header overhead extremely prohibitive so objects are entirely out of the question).
Most of the data is kept in contiguous memory mapped byte arrays.
This is hot code with an invocation count in the billions, so among the requirements is that it shouldn't allocate objects while at the same time being thread safe. That's a tricky combo.
Every while could be it's own function and now you have a bunch of simple unit tests. Unit tests are literally the double accounting for the logic, which is the value.
Any unit tests for that code is going to be horrendous to get decent coverage...and this is how it's easy to know it's too complex. Functions, especially if they are small, can be considered free, given the JVM inlines them into branches anyway....but I understand this is a hot path. If you want to avoid re-allocation, Java gets into your way. You could split up the function and use a singletonClass for holding the array, without having to pass the array by value and still being able to reference the singletonClass...blah blah blah.
> Uncle Bobbing this type of code doesn't make it much clearer
I get it and agree, while still recognizing the problem. Not you not the code not me. Java.
It's really unfortunate that Java has damaged programming practices so subtly and completely by being unnecessarily byzantine AND pushing horrible solutions like Spring.
bit data[length];
int width = 6;
bit value[width] = random(64);
for (i=0; i < lim; i += width) {
int j = endof(i, width);
data[i:j] = value;
}
or something like uint8_t c = 0xff;
c[0..3] = 1;
c[5..7] = 1;
// c == 0x31Otherwise, `std::vector<bool>` _may_ be specialized to occupy one bit per element [1].
[0]: https://en.cppreference.com/w/cpp/utility/bitset [1]: https://en.cppreference.com/w/cpp/container/vector_bool
public static byte[] func( uint p, uint q )
{
int pw = 32 - BitOperations.LeadingZeroCount( p );
int qw = 32 - BitOperations.LeadingZeroCount( q );
Span<byte> buff = stackalloc byte[ 9 ];
ulong val = (ulong)q | (ulong)p << qw;
BinaryPrimitives.WriteUInt64BigEndian( buff.Slice( 1 ), val );
int totalBytes = ( pw + qw + 7 ) / 8;
buff[ 8 - totalBytes ] = (byte)qw;
return buff.Slice( 8 - totalBytes ).ToArray();
}
In C++ about the same, albeit you gonna need either C++/20 language version, or some non-standard compiler specific intrinsics for bit scan and byte swap.To exploit this i had to use cython from python to define a c function which used a gcc compiler intrinsic to allow me to write the asm instruction inline. It turned out about 7 lines of code so it wasn’t as bad as it sounds.
In your case, you’d need to use JNI i suppose so it might not be any less code but it should at least be a lot faster if that matters.
ZZZZZZZZ,0000000Q,QQQQQQQQ,QQQQQQQQ,QPPPPPPP
With Z still being the width of P?Here's my attempt, which is shorter, and i think quite a bit clearer:
int pw = bitWidth(p);
int qw = bitWidth(q);
int qpw = qw + pw;
long qp = Integer.toUnsignedLong(q) << pw | Integer.toUnsignedLong(p);
int qpwBytes = ((qpw - 1) / Byte.SIZE) + 1;
byte[] bytes = new byte[qpwBytes + 1];
bytes[0] = (byte) pw;
for (int i = 1; i < bytes.length; i++) {
bytes[i] = (byte) (qp >> (qpwBytes - i) * Byte.SIZE & 0xff);
}
return bytes;
This did take me quite a bit of fiddling to get right - but it wasn't the bit-twiddling, it was the index arithmetic for copying the bytes into the array!https://docs.oracle.com/javase/7/docs/api/java/math/BigInteg...
Testing is not a panacea, by design you can only test for what you know and predict. In addition to testing, your setup needs to be resilient enough that unpredictable bugs can be solved quickly and won't lead to data loss.
I've also noticed a parallel phenomenon where teams double down on unit tests for branch conditions, coverage %, etc. when the bugs that are really hurting them predominantly cant even really be detected by unit tests.
My goal build pipeline brings up the app in docker-compose, then randomly kills services while running integration tests. So many failures are because people don't consider the happy path in a distributed/highly modular system.
Fuzz testing is still a type of testing.
Could fuzzing activate other kinds of bugs? Sure. But it's not magic. It's mostly working on known kinds of bugs.
If you put asserts everywhere in your code, to test all assumptions the code has, then fuzzing is an excellent way to see whenever one of those assumptions is violated because those violations are turned into crashes.
In my experience, fuzzing with extensive asserts is one of the best way to suss out bugs. It gets even better if you can take all of the paths the fuzzer found and run them through something like ASan or Valgrind.
You can read more about that at [1].
[1]: https://git.yzena.com/gavin/bc/src/branch/master/manuals/dev...
Programming errors are of special interest to programmers, as we tend to judge each other a bit harshly when these errors emerge as the problem is not on the business side or other teams making requirements.
In my experience working on many very large software, I have encountered one that was head and shoulder above the others in quality. This is not just a hunch. There were metrics tracked, thing like MTBF, and percent of sessions with clean exits, etc and this software was ridiculously better than the others.
The difference lied entirely on the fact that the better software had almost no unit test, but had 21K+ integration tests. I've worked on other software that also had more integration tests than average, and they too were of better quality.
The problem is making integration testing easy needs to be designed in from the start and requires not just one simple trick but multiple inter-locked design decisions that accumulate into making integration testing easy. In this particular case, one could write a new test just by using the software and a new test would be generated automatically. That's how you achieve writing 21k integration tests.
There are many unit test framework, but I've yet to see a generic integration framework. The reason is that integration tests are run with the whole software, so the whole software needs to be designed around them.
I'm interested in the topic. Could you talk more about it, or point to some resources describing in more details how this was achieved/what decisions had to be taken?
They might be a maintenance nightmare but... they'll probably be better than no tests
I just wanted to point out double bookkeeping analogy is bad.
Double bookkeeping is there to make certain types of errors very visible.
Double bookkeeping comes from idea that things do not just show up or disappear, but they change state -- value appearing on one account must have come from another. And so double bookkeeping is basically saying -- we want to have a system where it is immediately visible or even impossible to write something down that does not preserve this invariant.
It has nothing to do with whether the operation is accounted for correctly. You can still mess up accounts very easily.
Double bookkeeping does not mean double checking. You just select two accounts and put the same value on opposite sides of those accounts. This is a single operation. Everything about it can be wrong -- the value can be wrong, the accounts can be wrong and nothing is going to catch that error.
Actually, using invariants is one technique I use to ensure my code works correctly. Has nothing to do with unit tests. I just write code, whenever it is possible, in a way that makes it impossible to put it in a wrong state.
At the same time, my measuring stick is always, "Is the customer happy?" Software will never be perfect, so a zero bug rate is not a reasonable goal. Happy customers is quite a reasonable goal, and when they are not, their concerns direct where you need more quality.
NASA and nuclear power stations have a rather high cost to remediate some software defects, so it makes sense to work much harder to find them earlier. Same thing with anything life safety critical. You can't patch a bug and uncrash your space probe, or unmeltdown your powerplant, or unkill your patient. But a lot of other stuff is ok; yeah, it's not great if music players don't work on Jan 1 of years after a leap year, but you'll have four years for the product to decline into irrelevancy before that happens again (or to get patches out, if Zune had market fit)
> Do you really think NASA software is bug free?
Ignoring the fact you are arguing in bad faith is not compelling
GL with whatever.
After that point, everything is a compromise.
Sometimes the spec is a bit wrong, like forgetting to be explicit in precisely how the system should crash on a certain unexpected input.
End even then only if you stick to English strig hello world.
I have had hello worlds fail, in other languages :)
It is some kind of logical fallacy - just because really smart people worked on something and dedicated their lives to it doesn't mean it is good or correct or that it works.
It was sold as the "rolls royce of testing" which I think overstated its capabilities and effectiveness.
Model checking can be pretty productive relatively speaking, however.
Of the remaining problems, the complete, formal specification would be larger, more complex, and more bug-ridden than the implementation. "Hey adwn, can you add a button to the GUI so the user can export the current dataset to a CSV file?" Maybe 20-50 lines of code, but a full specification would be a multi-year project – and it would be almost certainly wrong.
And even if they can, where does that formal spec come from? Sooner or later, it comes from some informal understanding of what's supposed to happen. Well, how do you check that the formal spec is correct? Because if you can't do that, all formal verification can do is tell you that your program correctly implemented the wrong thing.
And I don't think you can do that. First, I don't think you can go from informal to formal by formal means. Second, even if you can, you still can't verify the informal spec. So formal verification can only go so far.
I can recall several things that were bugs in the spec. Log4j is the most recent example. Heartbleed I think was a specification bug. Back in the day, a lot of computer viruses were helped on their way by bad ideas in the specification of Microsoft Outlook.
It is pretty much impossible to write meaningful tests that cover everything.
This is especially true, when you mix complex, asynchronous server interactions, with random-access UI.
Today, I am fixing a couple of bugs in an app that interacts with three different servers (all asynchronously, but some semi-synchronously. The timing diagram is a bit ... intense), and also allows the user to do things like switch contexts, while some part of the server interaction is still unresolved.
I write a bit about my approach to testing, here: https://littlegreenviper.com/miscellany/testing-harness-vs-u...
Wanted to let you know that the "Here is the Doxygen-generated documentation for the BADGER layer" link is broken on this page: https://littlegreenviper.com/miscellany/forensic-design-docu...
I'll look at that.
But, of course, this is why we use CI.
It’s another (imo most important) level of correctness, unrelated to rigid math-like correctness of a result of programming of completely coherent requirements, which almost none of us ever receive.
Additionally with generated test values figuring out the validation logic becomes complex, and in complexity lies potential for bugs. If your testing code more complex than the code being tested, do you really gain that much confidence about the correctness? In comparison with hard-coded test values you can also hard-code the expected results, which can be gotten from some reference or just manually checked for correctness.
Of course ideally you'd have both random fuzzing and more manually defined tests, but that is setting quite high bar.
The author of this piece probably chose to make the post framework-agnostic by rolling their own random generation, but left that nuance out.
Because I'm a particular kind of idiot, it took me about 10 years of working in and around software engineering to understand that this is just not true. In many, many cases the most important goal for software is for it to take up some space in the market (either the external market or the internal corporate reputation market). In order for software to meet this goal, it must more or less function, but it doesn't need to be _correct_. It can crash, make mistakes, lose data, whatever.
In many situations this goal can be understood as "gathering capital." You write software to impress investors or to attract users or to convince other people in the corporate hierarchy that you are a going concern. Thus the valuable part of the software is not its correctness but its _surface_. How shiny is the software? Does it impress and/or please users? Does it impress investors?
If you've read Guy Debord you could have predicted this is how software would work. Software is spectacle.
In fields where that is the case, methods for ensuring correctness are important.
Most software is "usably wrong," which is good enough to build a career on.
Even more: Perfection takes a lot of time. Perfection therefore means less software reaching the user. So, is the imperfect software more useful to the user than no software at all? In most cases, yes, even with all the problems the software causes. (Because if it were otherwise, wouldn't the users stop using the software?)
TFA made a universal claim. OP replied “not true, here’s where it doesn’t hold.” Bringing up cases where it does hold doesn’t change anything.
Yup. And in many cases (2) doesn't matter at all - just heaping portions of (1)+(3).
You know the kind of "software" I'm talking about -- the kind that exists (and does all kinds of things) on pitch decks, or in conversations with gullible industry press types. But in no other sense.
Can I get paid to work on this software?
Will customers buy this software?
Is this software fit for some purpose?
Is the software correct according to what the customer expects?
Writing correct software is just a straightforward way of meeting customer expectations, which is a way to ensure that the software is fit for some purpose, which is a way to convince customers to buy the software, which is a way to ensure that you'll continue to be employed working on the software. It's not the only way to get paid, though.
(Sometimes software is developed by end users, in which case you can skip over the "will customers buy this?" question.)
"it can be difficult to add tests to a large application that has been developed entirely without testing. And that is why testing should be first on your mind when building serious software."
I've being doing it all my life. Join a new project, without any test, and start to add test code, while getting used with the code base. Actually, I would say that "adding tests" for a code base is the easiest and safest way to get used with the code base itself.
PSP = "Personal Software Process", the step before TSP, "Team Software Process".
Personal software process (PSP): https://en.wikipedia.org/wiki/Personal_software_process
Team software process (TSP): https://en.wikipedia.org/wiki/Team_software_process
It's there for anyone who is interested. Right now I'm skimming it to see what I can learn. Can be quite involved but can reduce errors and improve quality by orders of magnitude. (Proven.)
Given that, Humphrey repeatedly emphasizes that communication and understanding about what needs to be built are the most important parts, and that trying to test quality into larger systems can literally take years (of full-time work, by teams of dozens of developers).
Since I'm retired and reviewing all the ways that I wasted my life, then for me it's only an intellectual exercise, but this could help someone still in the thick of it. Lots of food for thought.
I read through the first chapter of PSP now, and this is exactly what I need! Thank you so much for sharing this.
Later on there is a mention of fuzzing. However, there is something better called property tests. Where the on failure there is automatic "shrinking" of input complexity to find a minimally failing test scenario.
For Erlang and Elixir I recommend https://propertesting.com/ book and the PropEr test framework https://github.com/proper-testing/proper.
As an example, here is the use of an advanced feature called targeted property based testing: https://proper-testing.github.io/tutorials/PropEr_testing_wi... used to test a labyrinth.
EDIT: as spockz mentioned below, the original idea was developed by QuviQ as QuickCheck http://www.quviq.com/products/erlang-quickcheck/. It's a commercial offering but there is a QuickCheck mini offered as a free download as well.
I test pure logic with property based testing and simple integration testing to ensure all the steps are aligned properly.
1) Define generators to produce input. These could start as random with some constraints. Say, "positive integers between 10 and 100" and then those can be combined in various ways with other generators like "positive integers between 10 and 100 in a tuple with a utf8 encoded binary between lengths 0 and 256" and so on.
2) Define properties which model your system. Given the inputs from generators, calling your application APIs should keep certain properties true. It should crash in only certain ways, or return only HTTP 200 responses, etc. These could be applied at any level from the simplest pure functions up to an HTTP API.
These steps don't have to be taking in the same order. I end up starting with 2 going back to 1, then 2 again etc.
The difference from basic fuzzing is that once you find a failure, it has a consistent and automatic way to backtrack and try to simplify the input down to a minimum which still causes the failure. So, if a giant 1Gb worth of JSON fails the fuzz test, it can be hard to see why it failed. With property testing, however, it might be simplified down a simple case with one utf8 encoded string of length 10 which has some specific emoji or something like that.
Consider an application with persistent state. Version 1 has a bug that introduces some slight inconsistency in the state file. Version 7 reads the state file, assumes that the state file is consistent, and ends up producing crazy results. Version 7 is "correct" but still fails.
One answer is to always validate the state file, but that may be impractical due to size or complexity.
A better answer is to use a database that offers declarative constraints that help prevent inconsistencies. This is such a good solution that something written in PHP could be very robust in practice if it uses a good database, whereas something written in haskell that uses a database without good constraints might fail miserably.
What about using duplicate user IDs?
Or maybe many objects in the system need both the employee ID and the name (and the employee ID determines the name, obviously), and the employee changes their name, but it only updates some objects and not all?
There are lots of ways data can be subtly inconsistent and a database is a big help preventing it.
I have 5-10 years programming experience and find an unlimited amount of bugs in other developer's work of any and all skill levels.
On occasion, something like a billing calculation will have a function doing the opposite of what they intend to do but somehow nobody has caught it in 5 years. I've also seen ancient security reports that just have a chunk of code that doesn't work like it sounds it should, causing 25% of results to be missed. These are just a couple of actual examples.
I focus on generally not screwing up my work like that as well as finding these problems in my team's code. It's mind blowing to me this has absolutely 0 value though. I and others like me are gatekept out of a lot of work since we process things differently. Developers can't seem to imagine a world where somebody thinks differently than them and memorizing leetcode is just as easy for everybody as it is them. "If you can't talk me through what you're doing while writing your memorized perfectly compilable code on a whiteboard or google doc, I guess you're either just lazy and not really invested, or a bad developer. Probably both."
The only thing that technically matters to get into the dev roles is memorizing leetcode problems in order to pass the interview so that A) You have a job at all (even small companies are doing these now)and B) You can get your actual salary corrected every couple years.
If it's not memorizing leetcode, it's how many (inefficient) lines of code did you contribute? (Thankfully this is finally starting to be phased out as a measurement AND bragging point.)
The people who make it through all this then go on to store their critical world-infrastructure Exchange version number in a 32 bit integer because "It worked and compiled when I tested it, so it's probably good enough." Nobody dares test it due to the toxic hostility back, or because a senior dev wrote it, or "I ran the code and it compiled for me, so it's good."
There's just so much talking down to others and gatekeeping about how leetcode solvers are superior and that it's the only possible starting block for a "real dev". I can't believe the frequency of simple yet major mistakes these people go on to actually do after they spend so much time bragging about it.
One guarantees the absence of certain classes of bugs; the other reduce the number of moving parts in a system.
If you tested your program, congratulations. Your program is now tested, incorrectly.
If you tested your program, and verified that the tests are correct, congratulations. Your program is now verified to do the wrong thing, correctly.
It has at least two other lines which I can't even think of the paraphrasing for.
The best bet, when writing (100%) correct code, is through thorough testing, and hoping for the best, because when you are handling a million lines of code, errors, will definitely creep up.
Personally, I feel achieving a 100% correct code is impossible, since developers are always updating, and adding new features to the code.
Hence why a team, should be put in place to create patches quickly, when bugs are found.
Sure it can. I've written 100% correct code using Coq. For example, I wrote a relatively simple program (~1.7k LoC) to interpret a simple programming language, but it was definitely correct (certified by a machine-checked proof).
Of course, for larger programs it's much harder to do that. But it's just a matter of how much time you're willing to invest.
If we can be convinced that we're 100% sure that 2+3=5, then what about a more complicated problem? What's the most complex math problem we can be sure about? What if we have to use a computer to check its correctness?
(In general, I think it's usually good enough to say we're pretty sure something is correct if we have some solid basis for believing that it is. I'm okay with being 99.99% sure that 2+3=5, but in the world of software "I'm 50% sure this software is correct" is a standard that most software I use on a daily basis fails to meet.)
I'm surprised at the lack of stack overflow jokes in this thread.
reply