Unfortunately, that fails to compile (the C code) with:
In file included from .atspkg/c/test/stack.c:14:
.atspkg/c/test/stack.c: In function
‘_057_home_057_vanessa_057_programming_057_ats_057_stack_057_SATS_057_stack_056_sats__push__1__1’:
.atspkg/c/test/stack.c:2884:21: error: variable or field
‘__atomic_compare_exchange_tmp’ declared void
2884 | ATSINSmove(tmp5__1,
atomic_compare_exchange_strong(ATSPMVrefarg1(arg0), tmpref3__1,
tmpref4__1)) ;
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In file included from .atspkg/c/test/stack.c:14:
.atspkg/c/test/stack.c:6958:21: error: argument 1 of
‘__atomic_compare_exchange’ must be a non-void pointer type
6958 | ATSINSmove(tmp5__2,
atomic_compare_exchange_strong(ATSPMVrefarg1(arg0), tmpref3__2,
tmpref4__2)) ;
| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
/home/vanessa/.atspkg/0.3.13/lib/ats2-postiats-0.3.13/ccomp/runtime/pats_ccomp_instrset.h:276:37:
note: in definition of macro ‘ATSINSmove’
276 | #define ATSINSmove(tmp, val) (tmp = val)
| ^~~
Since I guess C doesn't allow atomic void pointers for some reason?
Cheers,
Vanessa
On Friday, March 1, 2019 at 11:23:20 PM UTC-6, gmhwxi wrote:
>
>
> 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 ats-lan...@googlegroups.com <javascript:>.
>>> To post to this group, send email to ats-lan...@googlegroups.com
>>> <javascript:>.
>>> 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 ats-lang-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/361eb92b-ccfd-469e-9000-609ee524924b%40googlegroups.com.
