>
> I wonder if the same approach relating to memory allocation and free
> checking via static analysis could be applied to locking and unlocking of
> locks? I.e.:
Yes. See Dawson's papers. That is one of the examples given. Use after free is
one of the stock checkers. I don't think that there is a stock checker for
locks, it might be harder to infer lock/unlock then malloc/free. In which case
one would have to write an application specific lock check. In addition, in the
case of nested locks, the FSA used wouldn't suffice and one would have to call
out to C code. The first two are easy - I'd have to look at the MetaL manual to
figure out how difficult the third one is.
>
> - We don't release locks more than once.
>
> - We don't forget to unlock.
>
> - We hold a lock before accessing certain fields (defined by annotation)
> of a structure.
-Kip
_______________________________________________
[EMAIL PROTECTED] mailing list
http://lists.freebsd.org/mailman/listinfo/freebsd-hackers
To unsubscribe, send any mail to "[EMAIL PROTECTED]"
