Re: Dpkg in Ocaml
Claudio Sacerdoti Coen writes:
Hi,
Well, i am not really a coq user, so i don't know if this is actually
feasible. I was told it is possible though.
well, as a Coq user I think that it is _A_LOT_ of work to do that. Moreover:
1. dpkg is not really a critical application (no lost of human lifes,
no lost of money, etc.)
2. it is not even exactly clear to me _what_ do you want to prove.
For example, the FS operations of the kernel of Linux have been proven
correct in Coq, in the sense that it has been proven that no process can
read/write/execute a file if it has no right to do that. What do you want
to prove on the implementation of dpkg? It there is something interesting
to prove, maybe (maybe!) it could be worth the effort.
Cheers,
C.S.C.
Hello,
Well, i have never test anything with coq, but i kow that i will need it one
day or another...
When i tell dpkg corrupt some files, i talk about writing not syntactically
correct things in /var/lib/dpkg/status, for examples. A typical examples,
is that after trying to install something, let say ocaml-core, it rebuilds
/var/lib/dpkg/status by rewriting some parts of it. It fails ! Then i try
another time, and dpkg exit with failure code :
"error at line XXX in /var/lib/dpkg/status". When i edit this file i see
some weird things : for examples, it has rewrites badly the Depends field,
putting something like : Depends: lablgt@22k, ... I think this it typically
a dump of a corrupted memory area. I don't know much about it. I just know
that there is bug report against it, and that they have implemented a copy
mechanism ( before doing something, copy status to status.old ) because of
it.
So, the proof that will be needed here is that, when you rewrite status, you
rewrite it in the good way... I don't know if it is possible.
But off course, dpkg error are not danger for human life... But it could
put the system in an unstable state. For example, if it try again and again
to run dpkg, as status is not good, sometimes, it fails with an oops (
kernel
freeze )... In some environement it could be very dangerous.
I think there is a lot of work to do. But i don't say i will start to code
today, i am just asking : why not ? ( and in fact, after this problem i was
really thinking about it ).
Concerning memory :
The problem i describe has happen after a memory upgrade. I test the memory
with memtester for 100 hours. No errors occur. So i browse a little and find
that this problem has happen for other people. I think, but it is not an
affirmation, that there is some bugs lying around in the dpkg memory
management.
With ocaml, programmers don't care about memory management, could it be a
good way to bypass the memory problem of dpkg ?
I am really interested by your opinion. I just want to know, if it could
solve my problem.
Kind regard
Sylvain LE GALL
Reply to: