This is a simple RCU written in our language (https://github.com/anlun/OperationalSemanticsC11).

rcu.rkt

#lang at-exp racket
(require redex/reduction-semantics)
(require "../core/parser.rkt")

(define term_RCU
  @prog{ ;; Preparing visible state counters.
        cw_na    := 0;
        cr1_na   := 0;
        cr2_na   := 0;
        lhead_na := null;
        r0 := spw
              {{{ ;; Writer's thread.
                  ;; Creates a list with 1, 10, 100 values.
                  a_rlx     := [1 null];
                  ltail_rlx := a;
                  lhead_rel := a;

                  b_rlx     := [10 null];
                  rt        := ltail_rlx;
                  ltail_rel := [rt_1 b];
 
                  c_rlx     := [100 null];
                  rt        := ltail_rlx;
                  ltail_rel := [rt_1 c] 
              ||| r1 := spw
                        {{{ ;; First reader's thread.
                            sum1_na  := 0; ; Some value used as a result of list traversal.

                            ;; First list traversal.
                            rh      := lhead_con;
                            cur1_na := rh;                            
                            repeat
                              rCur := cur1_na;
                              if (rCur != null)
                              then rNode   := rCur_con;
                                   rSum    := sum1_na;
                                   sum1_na := rSum + rNode_1;
                                   cur1_na := rNode_2
                              else ret 0
                              fi 
                            end;
                            
                            ;; Starting quiescent State.
                            rC := wc_acq;
                            cr1_rel := rC;

                            ;; Second list traversal.
                            rh      := lhead_con;
                            cur1_na := rh;                            
                            repeat
                              rCur := cur1_na;
                              if (rCur != null)
                              then rNode   := rCur_con;
                                   rSum    := sum1_na;
                                   sum1_na := rSum + rNode_1;
                                   cur1_na := rNode_2
                              else ret 0
                              fi 
                            end;

                            sum1_na
                        ||| ;; Second reader's thread.
                            sum2_na  := 0; ; Some value used as a result of list traversal.

                            ;; First list traversal.
                            rh      := lhead_con;
                            cur2_na := rh;                            
                            repeat
                              rCur := cur2_na;
                              if (rCur != null)
                              then rNode   := rCur_con;
                                   rSum    := sum2_na;
                                   sum2_na := rSum + rNode_1;
                                   cur2_na := rNode_2
                              else ret 0
                              fi 
                            end;
                            
                            ;; Starting quiescent State.
                            rC := wc_acq;
                            cr2_rel := rC;

                            ;; Second list traversal.
                            rh      := lhead_con;
                            cur2_na := rh;                            
                            repeat
                              rCur := cur2_na;
                              if (rCur != null)
                              then rNode   := rCur_con;
                                   rSum    := sum2_na;
                                   sum2_na := rSum + rNode_1;
                                   cur2_na := rNode_2
                              else ret 0
                              fi 
                            end;

                            sum2_na
                        }}}
              }}} })

The number of statements in the writer's thread is 9. The number of execution steps to perform the first or second reader's thread can't be less then 14. Thus, a size of state space is more then 9 * 40,116,600 (http://betterexplained.com/articles/navigate-a-grid-using-combinations-and-permutations/). This makes this program non executable in reasonable time.