[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Bacula-devel] provability of correctness
Since I'm talking I'll add something else.
The biggest problem with bacula is that its behaviour is undocumented.
The behaviour of any system is given by its state diagram.
1. The initial state
2. The set of possible states
3. The set of transitions from any state
Lets leave out straight bugs. A Double Free is certainly a bad state,
but not where the problem lies.
The goal is that for all possible sets of jobs, timings, vols, media,
media type, status, autochangers, whatnot, bacula always works.
This is not true at the moment because we don't know what that set --the
If we did, we don't know that it correct.
Finally we don't know that the code bears any relation to the model.
What it does and what we think is does is different.
We are not alone, it was a key issue in the Denver airport baggage
Is this a real problem?
I say yes. I don't see many bugs which involve segfaults and do see bugs
where something doesn't work right.
Which is to say, bacula transitioned to an unexpected state.
Each time something is fixed, the risk is that something else is broken.
The equilibrium state is not where everything is fixed, but where
something is broken.
(The maths of it guarantees this)
What can be done?
Trying to work with the entirety of bacula is hopeless, but then, we
don't have to, because its already in nice chunks.
Divide and conquer. The smaller the parts the easier to work with.
The theory and practice of proof has received a lot of attention in the
last few years. The problem has been that the terms
in which the formal model is stated has been far from the mechanics of
This has now improved markedly with the mcrl2 project (www.mcrl2.org)
which has data types and structures more suited to
modelling a program.
Even if you think I'm full of crap, have a look at that site, the case
studies are interesting.
I think that getting a model will be hard work but worth it. This
technology is ideal for a smart young grad,
not easy for a oldster like me.
The map is not the territory.
So, we have a nice, provably correct, model. Then what? There is no
'generate code' button.
Working backwards from existing code to the model it implements isn't so
There are many independent processes in bacula and as soon as
conditionals and dependencies are added
the state space becomes immense.
What I am doing.
I'm rewriting the fd (read only) in part to get much better performance
with small files. Also
I hope to prove that my code is fault free. No deadlocks, livelocks or
Progress is slow, though. I hope to get a clear idea of the mechanics of
What you can do.
Think about it.
This SF.Net email is sponsored by the Moblin Your Move Developer's challenge
Build the coolest Linux based applications with Moblin SDK & win great prizes
Grand prize is a trip for two to an Open Source event anywhere in the world
Bacula-devel mailing list
This mailing list archive is a service of Copilot Consulting.