[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[FuSa SIG] TLA+/PlusCal

To: Fusa-sig <fusa-sig@xxxxxxxxxxxxxxxxxxxx>
From: Julien Grall <julien.grall@xxxxxxx>
Date: Wed, 14 Aug 2019 14:42:49 +0100
Cc: George Dunlap <george.dunlap@xxxxxxxxxxxxx>
Delivery-date: Wed, 14 Aug 2019 13:42:54 +0000
List-id: This is a discussion list for members of the Xen Project FuSa SIG <fusa-sig.lists.xenproject.org>

Hi all,

As discussed yesterday, Catalin Marinas (Arm64 Linux maintainers) has been usingTLA+/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

--
Julien Grall

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

Follow-Ups:
- Re: [FuSa SIG] TLA+/PlusCal
  - From: Rich Persaud

Prev by Date: [FuSa SIG] Call for Participation - Safety-Critical Systems Summit
Next by Date: Re: [FuSa SIG] TLA+/PlusCal
Previous by thread: [FuSa SIG] Call for Participation - Safety-Critical Systems Summit
Next by thread: Re: [FuSa SIG] TLA+/PlusCal
Index(es):
- Date
- Thread

Lists.xenproject.org is hosted with RackSpace, monitoring our
servers 24x7x365 and backed by RackSpace's Fanatical Support®.