fun print_racey (x:unit): cmd[unit] =
  cmd(
     spawn(cmd(val _ = cmd(print 'h') in
     spawn(cmd(val _ = cmd(print 'e') in
     spawn(cmd(val _ = cmd(print 'l') in
     spawn(cmd(val _ = cmd(print 'l') in
     spawn(cmd(val _ = cmd(print 'o') in
     spawn(cmd(val _ = cmd(print ' ') in
     spawn(cmd(val _ = cmd(print 'w') in
     spawn(cmd(val _ = cmd(print 'o') in
     spawn(cmd(val _ = cmd(print 'r') in
     spawn(cmd(val _ = cmd(print 'l') in
     spawn(cmd(val _ = cmd(print 'd') in
     spawn(cmd(val _ = cmd(print '!') in
     ret (<>))))))))))))))))))))))))));

fun print_safe (l:lock): cmd[unit] =
  cmd(
     val _ = acquire l in
     spawn(cmd(val _ = cmd(print 'h') in
     spawn(cmd(val _ = cmd(print 'e') in
     spawn(cmd(val _ = cmd(print 'l') in
     spawn(cmd(val _ = cmd(print 'l') in
     spawn(cmd(val _ = cmd(print 'o') in
     spawn(cmd(val _ = cmd(print ' ') in
     spawn(cmd(val _ = cmd(print 'w') in
     spawn(cmd(val _ = cmd(print 'o') in
     spawn(cmd(val _ = cmd(print 'r') in
     spawn(cmd(val _ = cmd(print 'l') in
     spawn(cmd(val _ = cmd(print 'd') in
     spawn(cmd(val _ = cmd(print '!') in
     spawn(cmd(val _ = release l      in
     ret (<>))))))))))))))))))))))))))));


fun race (x:unit): cmd[unit] =
  cmd(
    {spawn(print_racey(<>)),
     spawn(print_racey(<>)),
     spawn(print_racey(<>))});

fun no_race (x:unit): cmd[unit] =
  cmd(
    val l = new_lock (<>) in
    val _ = cmd(spawn(print_safe l)) in
    val _ = cmd(spawn(print_safe l)) in
    val _ = cmd(spawn(print_safe l)) in
    ret (<>));

do(race <>);
do(no_race <>);