Re: Writing a lock-free, threadsafe stack (or queue)

[Hongwei Xi]

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  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  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 
 %}

 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} (_t(a)? >> stack_t(a)) : void

 fun {a:vt@ype} push (_t(a) >> stack_t(a), a) : void

 fun {a:vt@ype} pop (_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)
 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 

Re: Writing a lock-free, threadsafe stack (or queue)

[Vanessa McHale]

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  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 
>>> %}
>>>
>>> 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} (_t(a)? >> stack_t(a)) : void
>>>
>>> fun {a:vt@ype} push (_t(a) >> stack_t(a), a) : void
>>>
>>> fun {a:vt@ype} pop (_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)
>>> 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 

Re: Writing a lock-free, threadsafe stack (or queue)

[Hongwei Xi]

I looked around this morning to see what approaches are used nowadays for
implementing
lock-free data structures. It seems that RCU is the way to go:
http://libcds.sourceforge.net/

With linear views, one should be able to capture some of the reasoning
behind RCUs, facilitating
the construction of lock-free data structures. Sounds like interesting
stuff, but I must focus on
implementing ATS3 for now :)


On Sat, Mar 2, 2019 at 10:35 AM Hongwei Xi  wrote:

> To share a global variable among threads without using a lock, one
> probably needs to introduce
> "special" views. For example, if a thread takes out a linear stack from
> the global vairable 'theStack',
> it cannot free it because it does not own the stack. I would think that
> linear views can help you reason
>
> When doing a lock-free implementation, please make sure that you do not
> modify the content obtained
> from reading a shared global variable except via a call to
> compare-and-swap.
>
> On Sat, Mar 2, 2019 at 8:23 AM Vanessa McHale 
> wrote:
>
>> Thanks!
>>
>> Is there any neat way to use views with a lock-free stack, then? I'm fine
>> ignoring frees for the moment, but it would be interesting to see how to do
>> such a thing safely in ATS...
>>
>> Cheers,
>> Vanessa
>> On 3/1/19 11:23 PM, 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  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 
 %}

 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} (_t(a)? >> stack_t(a)) : void

 fun {a:vt@ype} push (_t(a) >> stack_t(a), a) : void

 fun {a:vt@ype} pop (_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)
 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 

Re: Writing a lock-free, threadsafe stack (or queue)

[Vanessa McHale]

Thanks!

Is there any neat way to use views with a lock-free stack, then? I'm
fine ignoring frees for the moment, but it would be interesting to see
how to do such a thing safely in ATS...

Cheers,
Vanessa

On 3/1/19 11:23 PM, 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  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 
> %}
>
> 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} (_t(a)? >> stack_t(a)) : void
>
> fun {a:vt@ype} push (_t(a) >> stack_t(a), a) : void
>
> fun {a:vt@ype} pop (_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)
>     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-lang-users+unsubscr...@googlegroups.com
> .
> To post to this group, send email to
> ats-lang-users@googlegroups.com
> .
> Visit this group at
> https://groups.google.com/group/ats-lang-users
> .
> To view this discussion on the web visit
> 
> 

Re: Writing a lock-free, threadsafe stack (or queue)

[gmhwxi]

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  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 
>> %}
>>
>> 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} (_t(a)? >> stack_t(a)) : void
>>
>> fun {a:vt@ype} push (_t(a) >> stack_t(a), a) : void
>>
>> fun {a:vt@ype} pop (_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)
>> 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-lang-users+unsubscr...@googlegroups.com.
>> To post to this group, send email to ats-lang-users@googlegroups.com.
>> 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
>>  
>> 
>> .
>>
>

-- 
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 post to this group, send email to ats-lang-users@googlegroups.com.
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.

Re: Writing a lock-free, threadsafe stack (or queue)

[Hongwei Xi]

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 
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 
> %}
>
> 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} (_t(a)? >> stack_t(a)) : void
>
> fun {a:vt@ype} push (_t(a) >> stack_t(a), a) : void
>
> fun {a:vt@ype} pop (_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)
> 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-lang-users+unsubscr...@googlegroups.com.
> To post to this group, send email to ats-lang-users@googlegroups.com.
> 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
> 
> .
>

-- 
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 post to this group, send email to ats-lang-users@googlegroups.com.
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/CAPPSPLp7Lqi5TT_3FtGmuR8%3DdLmhMq5%3D1a_R4tOZSrwruyiw7g%40mail.gmail.com.

Re: Writing a lock-free, threadsafe stack (or queue)

[Vanessa McHale]

I don't think it's due to polymorphic functions, because the problem
goes away when I switch to using only one thread.

Cheers,
Vanessa

On 3/1/19 8:43 PM, Richard wrote:
> At first glance, making the functions polymorphic (as opposed to templates) 
> could be a potential reason for segmentation faults (see 
> https://github.com/githwxi/ATS-Postiats/issues/216). Though mixing dependent 
> types and templates together has also been known to cause issues (see 
> https://groups.google.com/d/msgid/ats-lang-users/c7885759-c97b-482e-a9a8-313152cc1e6b%40googlegroups.com?utm_medium=email_source=footer)
>
> On Thursday, February 28, 2019 at 12:10:50 PM UTC-5, Vanessa McHale 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 
>>
>>   %}
>>
>>   
>>
>>   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} (_t(a)? >> stack_t(a))
>> : void
>>
>>   
>>
>>   fun {a:vt@ype} push (_t(a) >> stack_t(a),
>> a) : void
>>
>>   
>>
>>   fun {a:vt@ype} pop (_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)
>>
>>       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-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
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/f4cf974c-6486-0064-d12d-292694bdf4a4%40iohk.io.


signature.asc
Description: OpenPGP digital signature

Re: Writing a lock-free, threadsafe stack (or queue)

[Richard]

At first glance, making the functions polymorphic (as opposed to templates) 
could be a potential reason for segmentation faults (see 
https://github.com/githwxi/ATS-Postiats/issues/216). Though mixing dependent 
types and templates together has also been known to cause issues (see 
https://groups.google.com/d/msgid/ats-lang-users/c7885759-c97b-482e-a9a8-313152cc1e6b%40googlegroups.com?utm_medium=email_source=footer)

On Thursday, February 28, 2019 at 12:10:50 PM UTC-5, Vanessa McHale 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 
> 
>   %}
> 
>   
> 
>   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} (_t(a)? >> stack_t(a))
> : void
> 
>   
> 
>   fun {a:vt@ype} push (_t(a) >> stack_t(a),
> a) : void
> 
>   
> 
>   fun {a:vt@ype} pop (_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)
> 
>       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-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
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/159f0461-8890-4dfe-9490-c31bb322d859%40googlegroups.com.