If we ignore malloc/free, then lock-free stack implementation
should look more or less like the following code:
fun
pop(theStack) = let
var xs0 = theStack
in
case+ xs0 of
| nil() => None_vt()
| cons(x0, xs1) =>
if atomic_compare_exchange(theStack, xs0, xs1)
then Some_vt(x0) else pop(theStack)
end
fun
push(theStack, x0) = let
var xs0 = theStack
val xs1 = cons(x0, xs0)
in
if atomic_compare_exchange(theStack, xs0, xs1) then () else
push(theStack, x0)
end
On Friday, March 1, 2019 at 11:05:44 PM UTC-5, gmhwxi wrote:
>
> I took a quick look.
>
> The paper gives an algorithm for implementing a queue, and your code
> implements
> a stack. The stack implementation contains a few race conditions. For
> example, say that thread A pops
> and thread B pops as well; after thread A frees a node, thread B could try
> to free it again, resulting in a very
> common crash caused by "double-free".
>
>
> On Thu, Feb 28, 2019 at 12:10 PM Vanessa McHale <vanessa...> wrote:
>
>> Hi all,
>>
>> I've been trying to implement a lock-free stack here:
>> https://github.com/vmchale/stack. Unfortunately, this is not something
>> I'm particularly familiar with, and it segfaults around 70% of the time I
>> try to actually do anything with it.
>>
>> Here is the static bit:
>>
>> %{#
>> #include <stdatomic.h>
>> %}
>>
>> typedef aptr(l: addr) = $extype "_Atomic void**"
>>
>> datavtype pointer_t(a: vt@ype) =
>> | pointer_t of node_t(a)
>> | none_t
>> and node_t(a: vt@ype) =
>> | node_t of @{ value = [ l : addr | l > null ] (a @ l | aptr(l))
>> , next = pointer_t(a)
>> }
>>
>> vtypedef stack_t(a: vt@ype) = @{ stack_head = pointer_t(a) }
>>
>> castfn release_stack {a:vt@ype} (stack_t(a)) : void
>>
>> fun new {a:vt@ype} (&stack_t(a)? >> stack_t(a)) : void
>>
>> fun {a:vt@ype} push (&stack_t(a) >> stack_t(a), a) : void
>>
>> fun {a:vt@ype} pop (&stack_t(a) >> _) : Option_vt(a)
>>
>> fun newm {a:vt@ype} () : stack_t(a)
>>
>> fn atomic_store {a:vt@ype}{ l : addr | l > null }(a? @ l | aptr(l), a) :
>> (a @ l | void) =
>> "mac#"
>>
>> fn atomic_load {a:vt@ype}{ l : addr | l > null }(a @ l | aptr(l)) : a =
>> "mac#"
>>
>> fn leaky_malloc {a:vt@ype}{ sz : int | sz == sizeof(a) }(sz : size_t(sz))
>> :
>> [ l : addr | l > null ] (a? @ l | aptr(l)) =
>> "mac#malloc"
>>
>> And here is the implementation:
>>
>> staload "SATS/stack.sats"
>>
>> implement new (st) =
>> st.stack_head := none_t
>>
>> implement {a} push (st, x) =
>> let
>> val (pf_pre | ptr) = leaky_malloc(sizeof<a>)
>> val (pf | ()) = atomic_store(pf_pre | ptr, x)
>> val next_node = node_t(@{ value = (pf | ptr), next = st.stack_head })
>> val () = st.stack_head := pointer_t(next_node)
>> in end
>>
>> implement {a} pop (st) =
>> case+ st.stack_head of
>> | ~pointer_t (~node_t (nd)) =>
>> begin
>> let
>> val (pf | aptr) = nd.value
>> val x = atomic_load(pf | aptr)
>> val () = st.stack_head := nd.next
>> in
>> Some_vt(x)
>> end
>> end
>> | none_t() => None_vt()
>>
>> It's based on the Michael-Scott paper
>> http://www.cs.rochester.edu/~scott/papers/1996_PODC_queues.pdf, but I
>> worry about the frees in the pattern match (of ~node_t and ~pointer_t),
>> and in fact this does segfault when I try to use it for parallel directory
>> traversal.
>>
>> Cheers,
>> Vanessa McHale
>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "ats-lang-users" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to [email protected].
>> To post to this group, send email to [email protected].
>> Visit this group at https://groups.google.com/group/ats-lang-users.
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/ats-lang-users/e1a19c62-5759-c930-4684-ffae2dec0813%40iohk.io
>>
>> <https://groups.google.com/d/msgid/ats-lang-users/e1a19c62-5759-c930-4684-ffae2dec0813%40iohk.io?utm_medium=email&utm_source=footer>
>> .
>>
>
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/d71163fe-91da-40c4-b68d-d605704a9db0%40googlegroups.com.
