From: stevenselectronicmail@gmail.com
Subject: Lock-Free stack in Ada SPARK
Date: Fri, 10 Feb 2017 19:07:42 -0800 (PST)
Date: 2017-02-10T19:07:42-08:00 [thread overview]
Message-ID: <c7c7fd16-9302-4ea0-99c0-c6c48c775348@googlegroups.com> (raw)
It's probably buggy. I still can't figure out how I'm supposed to prove properties about a volatile (protected) object.
https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-lock_free_stack.adb;h=ee17ba8dcff26527fa4f06dfa750d0846a16f255;hb=HEAD
There's also a lock-free condition variable like thing
https://sstewartgallus.com/git?p=linted.git;a=blob;f=src/ada-core/src/linted-wait_lists.adb;h=be46f99cb2907e13a37f2e848b901a4dcdd02109;hb=HEAD
next reply other threads:[~2017-02-11 3:07 UTC|newest]
Thread overview: 21+ messages / expand[flat|nested] mbox.gz Atom feed top
2017-02-11 3:07 stevenselectronicmail [this message]
2017-02-11 9:57 ` Lock-Free stack in Ada SPARK Hadrien Grasland
2017-02-11 10:07 ` Hadrien Grasland
2017-02-11 10:08 ` Hadrien Grasland
2017-02-11 10:14 ` Hadrien Grasland
2017-02-11 17:34 ` stevenselectronicmail
2017-02-11 19:36 ` Jeffrey R. Carter
2017-02-11 20:42 ` stevenselectronicmail
2017-02-11 22:40 ` Dmitry A. Kazakov
2017-02-11 23:02 ` stevenselectronicmail
2017-02-12 8:30 ` Dmitry A. Kazakov
2017-02-12 12:26 ` Hadrien Grasland
2017-02-12 12:49 ` Dmitry A. Kazakov
2017-02-12 13:19 ` Hadrien Grasland
2017-02-12 14:57 ` Dmitry A. Kazakov
2017-02-12 13:04 ` Hadrien Grasland
2017-02-12 22:25 ` Robert Eachus
2017-02-13 8:22 ` Dmitry A. Kazakov
2017-02-13 20:04 ` stevenselectronicmail
2017-02-21 1:51 ` Robert Eachus
2017-02-21 8:44 ` Dmitry A. Kazakov
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox