raco symtrace errors with "another client is already connected"

[c0nn3r]

When running raco symtrace I get the following error (even if no client is running).

> okefenokee:testing-rosette conner$ raco symtrace main.rkt
Your Web application is running at http://localhost:8000/?port=8048&title=main.rkt.
Stop this program at any time to terminate the Web Server.
unexpected response from client "another client is already connected"
  context...:
   body of "/opt/homebrew/Cellar/minimal-racket/8.1/share/racket/pkgs/rosette/rosette/lib/trace/raco.rkt"
   /opt/homebrew/Cellar/minimal-racket/8.1/share/racket/collects/raco/raco.rkt:41:0
   body of "/opt/homebrew/Cellar/minimal-racket/8.1/share/racket/collects/raco/raco.rkt"
   body of "/opt/homebrew/Cellar/minimal-racket/8.1/share/racket/collects/raco/main.rkt"

[sorawee]

Hmm. It works fine on my computer. To help us debugging this, could you provide us main.rkt or a program that will trigger the error? Also, when you run an example program from the Debugging chapter. Say:

#lang rosette

(define-symbolic xs integer? #:length 4)
(define (sum xs) (foldl + xs)) ; bug: missing 0 after +
(verify (assert (= (sum xs) (sum (filter-not zero? xs)))))

Do you get an error as well?

[c0nn3r]

I don't get it when I run the example program in the Debugging Chapter. I think I get it when I use synthesize.

Sorry for the long program.

#lang rosette

(require rosette/lib/synthax)

(define int32? (bitvector 32))

(define-symbolic x int32?)
(define-symbolic a b c d e f g int32?)

(define (int32 i)
  (bv i int32?))

(define (single-digit-hash x)
  (set! x (bvxor (bvlshr x (?? int32?))))
  (set! x (bvmul (bvlshr x (?? int32?))))
  (set! x (bvxor (bvlshr x (?? int32?))))
  (set! x (bvmul (bvlshr x (?? int32?))))
  (set! x (bvxor (bvlshr x (?? int32?))))
  x)

(define (hand-rank a b c d e f g)
  (bvsmod
    (foldr bvxor (int32 0) (map single-digit-hash '(a b c d e f g)))) (int32 7462))

(define sol
  (synthesize
   #:forall (list a b c d e f g)
   #:guarantee
   (begin
    (assume (bvslt a (int32 52)))
    (assume (bvslt b (int32 52)))
    (assume (bvslt c (int32 52)))
    (assume (bvslt d (int32 52)))
    (assume (bvslt e (int32 52)))
    (assume (bvslt f (int32 52)))
    (assume (bvslt g (int32 52)))

    (assume (bvsgt a (int32 0)))
    (assume (bvsgt b (int32 0)))
    (assume (bvsgt c (int32 0)))
    (assume (bvsgt d (int32 0)))
    (assume (bvsgt e (int32 0)))
    (assume (bvsgt f (int32 0)))
    (assume (bvsgt g (int32 0)))

    (for ([line (file->lines "1.tsv")])
      (let ([split (string-split line "\t")])
    (let ([cards
        (map int32 (map string->number (string-split (car split) " ")))]
          [value (int32 (string->number (string-trim (cdr split))))])
      (assert (equal? (hand-rank cards) value))))))))

(print-forms sol)

Where 1.tsv is:

44 9 48 37 24 26 42 2616

[sorawee]

Yes, I can reproduce it now. Will try to fix this over this weekend. Thanks for the report!

[c0nn3r]

Thanks so much!

[sorawee]

I assume that you are using Mac M1. Is that correct?

The problem seems to be due to the CAS (compare-and-swap) operation, which is not reliable on ARM processors. I submitted a PR that retries the operation again on failure, and it seems to help with the problem on my computer.

[c0nn3r]

Wow, you are good 😳 Yes, I am using a M1 Mac.

Interesting, I would have never figured this out, thank you for the fix!