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

[Vanessa McHale]

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

[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&utm_source=footer)

[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

[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".

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

[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".

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-users+unsubscribe@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.

[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

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@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.

--



Vanessa McHale
Functional Compiler Engineer | Chicago, IL

Website: www.iohk.io
Twitter: @vamchale
PGP Key ID: 4209B7B5






This e-mail and any file transmitted with it are confidential and intended solely for the use of the recipient(s) to whom it is addressed. Dissemination, distribution, and/or copying of the transmission by anyone other than the intended recipient(s) is prohibited. If you have received this transmission in error please notify IOHK immediately and delete it from your system. E-mail transmissions cannot be guaranteed to be secure or error free. We do not accept liability for any loss, damage, or error arising from this transmission

[Hongwei Xi]

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.

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@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.

--



Vanessa McHale
Functional Compiler Engineer | Chicago, IL

Website: www.iohk.io
Twitter: @vamchale
PGP Key ID: 4209B7B5






This e-mail and any file transmitted with it are confidential and intended solely for the use of the recipient(s) to whom it is addressed. Dissemination, distribution, and/or copying of the transmission by anyone other than the intended recipient(s) is prohibited. If you have received this transmission in error please notify IOHK immediately and delete it from your system. E-mail transmissions cannot be guaranteed to be secure or error free. We do not accept liability for any loss, damage, or error arising from this transmission

--
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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@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/b8107961-a4b5-5222-ac08-6d85f885643f%40iohk.io.

[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 :)

[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

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lan...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.

[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).

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@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.