[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 
model-- is.
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 
handling debacle.

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

Why bacula?
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 
unprotected data.
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.