search

runtimeverification / rv-predict

Code for improved rv-predict and installer
BSD 3-Clause "New" or "Revised" License
2 stars 3 forks source link

Knot races #1013

Open maya-rv opened 5 years ago

maya-rv commented 5 years ago

This is the output, and I have to write it down somewhere in order to discuss it. I only managed to get knot to answer with REFUSED, but I tried to run knotc and reloaded configuration a bunch, which is the likely trigger for these reports, once knot is killed.

Data race on [0x00000000013bdbb1 : 0x000000000042fbf1/0x00007fdd65a7dae0]:
    Read in thread 2 holding lock [0x00000000013bdb58 : 0xffffffffffffffff/0x0000000000000000]
      > in worker_main at knot/worker/pool.c:65
      - locked [0x00000000013bdb58 : 0xffffffffffffffff/0x0000000000000000] worker_main at knot/worker/pool.c:60
        in thread_ep at knot/server/dthreads.c:146
    Thread 2 created by thread 1
      > in dt_start at knot/server/dthreads.c:441

    Write in thread 1 holding lock [0x00000000013bdb58 : 0x000000000042ff5a/0x00007ffc8618cef0]
      > in worker_pool_resume at knot/worker/pool.c:180
      - locked [0x00000000013bdb58 : 0x000000000042ff5a/0x00007ffc8618cef0] worker_pool_resume at knot/worker/pool.c:180
        in server_update_zones at knot/server/server.c:898
        in server_reload at knot/server/server.c:689
        in ctl_server at knot/ctl/commands.c:1442
        in ctl_exec at knot/ctl/commands.c:1854
        in ctl_process at knot/ctl/process.c:96
        in main at utils/knotd/main.c:269
    Thread 1 is the main thread

    Undefined behavior (UB-CEER4):
        see C11 section 5.1.2.4:25 http://rvdoc.org/C11/5.1.2.4
        see C11 section J.2:1 item 5 http://rvdoc.org/C11/J.2
        see CERT-C section MSC15-C http://rvdoc.org/CERT-C/MSC15-C
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

Data race on [0x00000000013bc9e0 : 0x000000000042cfa7/0x00007fdd40434ae0]:
    Write in thread 1
      > in server_reconfigure at knot/server/server.c:386
        in server_reload at knot/server/server.c:682
        in server_reload at knot/server/server.c:682
        in ctl_server at knot/ctl/commands.c:1442
        in ctl_exec at knot/ctl/commands.c:1854
        in ctl_process at knot/ctl/process.c:96
        in main at utils/knotd/main.c:269
    Thread 1 is the main thread

    Read in thread 25
      > in tcp_master at knot/server/tcp-handler.c:332
        in thread_ep at knot/server/dthreads.c:146
    Thread 25 created by thread 1
      > in dt_start at knot/server/dthreads.c:441

    Undefined behavior (UB-CEER4):
        see C11 section 5.1.2.4:25 http://rvdoc.org/C11/5.1.2.4
        see C11 section J.2:1 item 5 http://rvdoc.org/C11/J.2
        see CERT-C section MSC15-C http://rvdoc.org/CERT-C/MSC15-C
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

Data race on [0x00000000013bc080 : 0x000000000042a0fa/0x00007fdd40434820]:
    Write in thread 1 holding locks [0x00000000013d75f0 : 0x0000000000429ec7/0x00007ffc8618cd10], [0x00000000013bc0f0 : 0x0000000000429f13/0x00007ffc8618cd10]
      > in dt_update_thread at knot/server/dthreads.c:81
      - locked [0x00000000013bc0f0 : 0x0000000000429f13/0x00007ffc8618cd10] dt_update_thread at knot/server/dthreads.c:41
      - locked [0x00000000013d75f0 : 0x0000000000429ec7/0x00007ffc8618cd10] dt_update_thread at knot/server/dthreads.c:38
        in dt_activate at knot/server/dthreads.c:629
        in server_reconfigure at knot/server/server.c:390
        in server_reload at knot/server/server.c:682
        in server_reload at knot/server/server.c:682
        in ctl_server at knot/ctl/commands.c:1442
        in ctl_exec at knot/ctl/commands.c:1854
        in ctl_process at knot/ctl/process.c:96
        in main at utils/knotd/main.c:269
    Thread 1 is the main thread

    Read in thread 25
      > in dt_is_cancelled at knot/server/dthreads.c:721
        in tcp_master at knot/server/tcp-handler.c:350
        in thread_ep at knot/server/dthreads.c:146
    Thread 25 created by thread 1
      > in dt_start at knot/server/dthreads.c:441

    Undefined behavior (UB-CEER4):
        see C11 section 5.1.2.4:25 http://rvdoc.org/C11/5.1.2.4
        see C11 section J.2:1 item 5 http://rvdoc.org/C11/J.2
        see CERT-C section MSC15-C http://rvdoc.org/CERT-C/MSC15-C
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

Data race on [0x00000000013d7570 : 0x000000000042eed7/0x00007fdd64f72ae0]:
    Write in thread 1
      > in server_reconfigure at knot/server/server.c:387
        in server_reload at knot/server/server.c:682
        in server_reload at knot/server/server.c:682
        in ctl_server at knot/ctl/commands.c:1442
        in ctl_exec at knot/ctl/commands.c:1854
        in ctl_process at knot/ctl/process.c:96
        in main at utils/knotd/main.c:269
    Thread 1 is the main thread

    Read in thread 13
      > in udp_master at knot/server/udp-handler.c:454
        in thread_ep at knot/server/dthreads.c:146
    Thread 13 created by thread 1
      > in dt_start at knot/server/dthreads.c:441

    Undefined behavior (UB-CEER4):
        see C11 section 5.1.2.4:25 http://rvdoc.org/C11/5.1.2.4
        see C11 section J.2:1 item 5 http://rvdoc.org/C11/J.2
        see CERT-C section MSC15-C http://rvdoc.org/CERT-C/MSC15-C
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

Data race on [0x00000000013d7534 : 0x000000000042eed7/0x00007fdd64e71ae0]:
    Read in thread 1
      > in server_reconfigure at knot/server/server.c:371
        in server_reload at knot/server/server.c:682
        in server_reload at knot/server/server.c:682
        in ctl_server at knot/ctl/commands.c:1442
        in ctl_exec at knot/ctl/commands.c:1854
        in ctl_process at knot/ctl/process.c:96
        in main at utils/knotd/main.c:269
    Thread 1 is the main thread

    Write in thread 14
      > in udp_master at knot/server/udp-handler.c:453
        in thread_ep at knot/server/dthreads.c:146
    Thread 14 created by thread 1
      > in dt_start at knot/server/dthreads.c:441

    Undefined behavior (UB-CEER4):
        see C11 section 5.1.2.4:25 http://rvdoc.org/C11/5.1.2.4
        see C11 section J.2:1 item 5 http://rvdoc.org/C11/J.2
        see CERT-C section MSC15-C http://rvdoc.org/CERT-C/MSC15-C
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1

Data race on [0x00000000013d7530 : 0x000000000042eed7/0x00007fdd64f72ae0]:
    Write in thread 1
      > in server_reconfigure at knot/server/server.c:386
        in server_reload at knot/server/server.c:682
        in server_reload at knot/server/server.c:682
        in ctl_server at knot/ctl/commands.c:1442
        in ctl_exec at knot/ctl/commands.c:1854
        in ctl_process at knot/ctl/process.c:96
        in main at utils/knotd/main.c:269
    Thread 1 is the main thread

    Read in thread 13
      > in udp_master at knot/server/udp-handler.c:452
        in thread_ep at knot/server/dthreads.c:146
    Thread 13 created by thread 1
      > in dt_start at knot/server/dthreads.c:441

    Undefined behavior (UB-CEER4):
        see C11 section 5.1.2.4:25 http://rvdoc.org/C11/5.1.2.4
        see C11 section J.2:1 item 5 http://rvdoc.org/C11/J.2
        see CERT-C section MSC15-C http://rvdoc.org/CERT-C/MSC15-C
        see MISRA-C section 8.1:3 http://rvdoc.org/MISRA-C/8.1
maya-rv commented 5 years ago

The first one:

Data race on [0x00000000013bdbb1 : 0x000000000042fbf1/0x00007fdd65a7dae0]:
    Read in thread 2 holding lock [0x00000000013bdb58 : 0xffffffffffffffff/0x0000000000000000]
      > in worker_main at knot/worker/pool.c:65
...
    Write in thread 1 holding lock [0x00000000013bdb58 : 0x000000000042ff5a/0x00007ffc8618cef0]
      > in worker_pool_resume at knot/worker/pool.c:180

The code looks as follows:

 57         pthread_mutex_lock(&pool->lock);
 58 
 59         for (;;) {
 65                 if (k = worker_queue_dequeue(&pool->tasks);
 67                 }
pool->suspended) {
 66                         task = worker_queue_dequeue(&pool->tasks);
 67                 }
179         pthread_mutex_lock(&pool->lock);
180         pool->suspended = false;
181         pthread_cond_broadcast(&pool->wake);
182         pthread_mutex_unlock(&pool->lock);

I don't understand why predict is complaining at all. It is even stating both cases are under lock. What is it reporting?

maya-rv commented 5 years ago

The second case is as follows:

Data race on [0x00000000013bc9e0 : 0x000000000042cfa7/0x00007fdd40434ae0]:
    Write in thread 1
          > in server_reconfigure at knot/server/server.c:386

380         /* Update TCP+UDP ifacelist (reload all threads). */
381         unsigned thread_count = 0;
382         for (unsigned proto = IO_UDP; proto <= IO_TCP; ++proto) {
383                 dt_unit_t *tu = s->handlers[proto].handler.unit;
384                 for (unsigned i = 0; i < tu->size; ++i) {
385                         ref_retain((ref_t *)newlist);
386                         s->handlers[proto].handler.thread_state[i] |= ServerReload;

    Read in thread 25
          > in tcp_master at knot/server/tcp-handler.c:332

295         unsigned *iostate = &handler->thread_state[dt_get_id(thread)];

329         for(;;) {
330 
331                 /* Check handler state. */
332                 if (unlikely(*iostate & ServerReload)) {
333                         *iostate &= ~ServerReload;

this isn't an interesting race: a given's thread thread_state has only one possible reader and only one possible writer. it might be marginally interesting to keep reporting this, the fact it isn't problematic relies on how "a write to unsigned is atomic", and I suspect this isn't guaranteed for all architectures.

gnuoyd commented 5 years ago

This may be more than one issue. I'm labelling it runtime, for now. I think the condvar branch will fix this, but it's tricky to merge to master because it makes a number of changes to how the runtime's function interposition works, and it stops us from suppressing system symbols in the reports.