C does not allow any field (in a struct) to be of the type void.
I assume that you did something like pointer(void). If so, please
try pointer(int) or pointer(ptr).





On Fri, Oct 25, 2019 at 3:25 PM Vanessa McHale <[email protected]> wrote:

> 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 [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 view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/361eb92b-ccfd-469e-9000-609ee524924b%40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/361eb92b-ccfd-469e-9000-609ee524924b%40googlegroups.com?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 view this discussion on the web visit 
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLptHzwdpjOK9j0h4NXvphVpr8255%2BHtFos-2k_0YTxqRw%40mail.gmail.com.

Reply via email to