Re: [FuSa SIG] TLA+/PlusCal

[Rich Persaud <persaur@xxxxxxxxx>]

On Aug 14, 2019, at 09:42, Julien Grall <julien.grall@xxxxxxx> wrote:

Hi all,

As discussed yesterday, Catalin Marinas (Arm64 Linux maintainers) has been using TLA+/PlusCal to prove some part of the Linux kernel (ticketlock, qspinlock...). For some examples see [1].

He actually managed to find race conditions in some of the algorithm :).

I can introduce Catalin to anyone interested with TLA+/PlusCal.

Cheers,

[1]  https://git.kernel.org/pub/scm/linux/kernel/git/cmarinas/kernel-tla.git

Thomas Leonard (MirageOS Xen subproject, used in QubesOS firewall) has applied TLA+ to understand vchan protocol ambiguities. 

http://roscidus.com/blog/blog/2019/01/01/using-tla-plus-to-understand-xen-vchan/

He has licensed his work as BSD 2-clause, so it can be incorporated into Xen documentation:

https://github.com/talex5/spec-vchan

Rich

_______________________________________________
Fusa-sig mailing list
Fusa-sig@xxxxxxxxxxxxxxxxxxxx
https://lists.xenproject.org/mailman/listinfo/fusa-sig