Online Linux Driver Verification Service (alpha)

Rule violation
Driver: xordev.tar.gz
Kernel: linux-2.6.37
Verification architecture: x86_64
Rule: Spinlocks lock/unlock
Error trace
Function bodies
Blocks
  • Others...
    Entry point
    Entry point body
    Function calls
    Initialization function calls
    Function without body calls
    Function stack overflows
    Initialization function bodies
    Returns
    Return values
    Asserts
    Assert conditions
    Identation
    Driver environment initialization
    Driver environment function calls
    Driver environment function bodies
    Model asserts
    Model state changes
    Model returns
    Model function calls
    Model function bodies
    Model function function calls
    Model function function bodies
    Model others
    Function bodies without model function calls
Hide Entry point Hide Entry point body Hide Function calls Show Initialization function calls Hide Function without body calls Hide Function stack overflows Hide Function bodies Show Initialization function bodies Hide Blocks Hide Returns Hide Return values Hide Asserts Hide Assert conditions Hide Identation Show Driver environment initialization Hide Driver environment function calls Hide Driver environment function bodies Hide Model asserts Hide Model state changes Hide Model returns Hide Model function calls Show Model function bodies Hide Model function function calls Hide Model function function bodies Hide Model others Show Function bodies without model function calls
-entry_point();
{
559 LDV_IN_INTERRUPT = 1;
568 +ldv_initialize_FOREACH();
584 +tmp___7 = xordev_init_module();
584 assert(tmp___7 == 0);
589 tmp___9 = nondet_int() { /* The function body is undefined. */ };
589 assert(tmp___9 != 0);
592 tmp___8 = nondet_int() { /* The function body is undefined. */ };
594 assert(tmp___8 == 0);
597 LDV_IN_INTERRUPT = 2;
612 -xordev_irq_handler(var_xordev_irq_handler_12_p0 /* irq */, var_xordev_irq_handler_12_p1 /* device */);
{
311 +tmp___7 = pci_get_drvdata(device /* pdev */);
311 xordev = tmp___7;
315 +ldv_spin_lock_irqsave_lock(&(xordev)->lock /* lock */, irq_flags /* flags */);
316 tmp___8 = ioread32(*(xordev).iomem + REG_INTR_EN) { /* The function body is undefined. */ };
316 assert(tmp___8 == IRQ_ON);
320 tmp___9 = ioread32(*(xordev).iomem + REG_COUNT) { /* The function body is undefined. */ };
320 count = tmp___9;
321 tmp___10 = ioread32(*(xordev).iomem + REG_INTR_COUNT) { /* The function body is undefined. */ };
321 intr_count = tmp___10;
322 assert(count <= intr_count);
328 -update_buffer(*(xordev).src1 /* chardev */);
{
107 buffer = *(chardev).buffer;
111 +ldv_spin_lock_irqsave_lock(&(buffer)->lock /* lock */, irq_flags /* flags */);
}
}
}
Source code
1 #include <linux/spinlock.h> 2 void ldv_spin_lock_irqsave(spinlock_t *lock, unsigned long flags); 3 void ldv_spin_lock_nested(spinlock_t *lock, int subclass); 4 void ldv_spin_lock_nest_lock(spinlock_t *lock, void *map); 5 void ldv_spin_lock_irqsave_nested(spinlock_t *lock, int subclass); 6 int ldv_spin_trylock_irqsave(spinlock_t *lock, unsigned long flags); 7 void ldv_spin_lock(spinlock_t *lock); 8 void ldv_spin_lock_bh(spinlock_t *lock); 9 void ldv_spin_lock_irq(spinlock_t *lock); 10 int ldv_spin_trylock(spinlock_t *lock); 11 int ldv_spin_trylock_bh(spinlock_t *lock); 12 int ldv_spin_trylock_irq(spinlock_t *lock); 13 void ldv_spin_unlock(spinlock_t *lock); 14 void ldv_spin_unlock_bh(spinlock_t *lock); 15 void ldv_spin_unlock_irq(spinlock_t *lock); 16 void ldv_spin_unlock_irqrestore(spinlock_t *lock, unsigned long flags); 17 void ldv_spin_unlock_wait(spinlock_t *lock); 18 int ldv_spin_is_locked(spinlock_t *lock); 19 int ldv_spin_is_contended(spinlock_t *lock); 20 int ldv_spin_can_lock(spinlock_t *lock); 21 int ldv_atomic_dec_and_lock(spinlock_t *lock, atomic_t *atomic); 22 #define ldv_atomic_dec_and_lock_macro(atomic,lock) ldv_atomic_dec_and_lock(lock,atomic) 23 // Michal Marschall 24 // Numer indeksu: 291693 25 26 #include "circ_dma_buf.h" 27 #include <linux/kernel.h> 28 #include <linux/pci.h> 29 30 const int CDB_SIZE = 4096; 31 32 struct circ_dma_buf *cdb_alloc(struct device *device) { 33 struct circ_dma_buf *buffer = kmalloc(sizeof(struct circ_dma_buf), GFP_KERNEL); 34 if(buffer == NULL) 35 return NULL; 36 buffer->data = dma_alloc_coherent(device, CDB_SIZE, &buffer->handle, GFP_KERNEL); 37 if(buffer->data == NULL) { 38 kfree(buffer); // avoid memory leak 39 return NULL; 40 } 41 buffer->start = 0; 42 buffer->fill = 0; 43 buffer->device = device; 44 spin_lock_init(&buffer->lock); 45 return buffer; 46 } 47 48 void cdb_free(struct circ_dma_buf *buffer) { 49 dma_free_coherent(buffer->device, CDB_SIZE, buffer->data, buffer->handle); 50 kfree(buffer); 51 } 52 53 int cdb_inc_begin(struct circ_dma_buf *buffer, int value) { 54 if(value > buffer->fill) 55 value = buffer->fill; 56 buffer->fill -= value; 57 buffer->start = (buffer->start + value) % CDB_SIZE; 58 return value; 59 } 60 61 int cdb_inc_end(struct circ_dma_buf *buffer, int value) { 62 if(value > CDB_SIZE - buffer->fill) 63 value = CDB_SIZE - buffer->fill; 64 buffer->fill += value; 65 return value; 66 } 67 68 int cdb_copy_from(struct circ_dma_buf *source, void *dest, int count, int (*copy_func)(void *, void *, int)) { 69 int first, copied1, copied2; 70 unsigned long irq_flags; 71 72 ldv_spin_lock_irqsave(&source->lock, irq_flags); 73 if(count > source->fill) 74 count = source->fill; 75 76 // copy first part: 77 if(count > CDB_SIZE - source->start) 78 first = CDB_SIZE - source->start; 79 else 80 first = count; 81 ldv_spin_unlock_irqrestore(&source->lock, irq_flags); 82 copied1 = copy_func(source->data + source->start, dest, first); 83 ldv_spin_lock_irqsave(&source->lock, irq_flags); 84 cdb_inc_begin(source, copied1); 85 ldv_spin_unlock_irqrestore(&source->lock, irq_flags); 86 if(first == count || copied1 < first) // copied everything or error 87 return copied1; 88 89 // copy second part: 90 copied2 = copy_func(source->data, dest + first, count - first); 91 cdb_inc_begin(source, copied2); 92 93 return copied1 + copied2; 94 } 95 96 int cdb_copy_to(void *source, struct circ_dma_buf *dest, int count, int (*copy_func)(void *, void *, int)) { 97 int end, first, copied1, copied2; 98 unsigned long irq_flags; 99 100 ldv_spin_lock_irqsave(&dest->lock, irq_flags); 101 if(count > CDB_SIZE - dest->fill) 102 count = CDB_SIZE - dest->fill; 103 104 // copy first part: 105 end = (dest->start + dest->fill) % CDB_SIZE; 106 if(end + count > CDB_SIZE) 107 first = CDB_SIZE - end; 108 else 109 first = count; 110 ldv_spin_unlock_irqrestore(&dest->lock, irq_flags); 111 copied1 = copy_func(source, dest->data + end, first); 112 ldv_spin_lock_irqsave(&dest->lock, irq_flags); 113 cdb_inc_end(dest, copied1); 114 ldv_spin_unlock_irqrestore(&dest->lock, irq_flags); 115 if(first == count || copied1 < first) // copied everything or error 116 return copied1; 117 118 // copy second part: 119 copied2 = copy_func(source + first, dest->data, count - first); 120 cdb_inc_end(dest, copied2); 121 122 return copied1 + copied2; 123 } 124 /* LDV_COMMENT_BEGIN_MODEL */ 125 #include <linux/kernel.h> 126 #include <linux/spinlock.h> 127 128 /* 129 CONFIG_DEBUG_SPINLOCK should be true 130 make menuconfig 131 Kernel hacking->Kernel debugging->Spinlock and rw-lock debugging: basic checks 132 */ 133 134 /* the function works only without aspectator */ 135 long __builtin_expect(long val, long res) { 136 return val; 137 } 138 139 #include "engine-blast.h" 140 141 142 /* Need this because rerouter is buggy!.. */ 143 extern int ldv_lock_TEMPLATE; 144 /* Now the actual variable goes... */ 145 int ldv_lock_TEMPLATE = 1; 146 147 #define __ldv_spin_lock() \ 148 do {\ 149 /* LDV_COMMENT_ASSERT Lock should be in a free state*/\ 150 ldv_assert(ldv_lock_TEMPLATE==1);\ 151 /* LDV_COMMENT_CHANGE_STATE Goto locked state*/\ 152 ldv_lock_TEMPLATE=2;\ 153 } while(0) 154 155 #define __ldv_spin_unlock() \ 156 do {\ 157 /* LDV_COMMENT_ASSERT Lock should be in a locked state*/\ 158 ldv_assert(ldv_lock_TEMPLATE!=1);\ 159 /* LDV_COMMENT_CHANGE_STATE Goto free state*/\ 160 ldv_lock_TEMPLATE=1;\ 161 } while(0) 162 163 #define __ldv_spin_trylock() \ 164 do {\ 165 int is_lock_held_by_another_thread;\ 166 /* LDV_COMMENT_OTHER Construct an arbitrary flag*/\ 167 is_lock_held_by_another_thread = ldv_undef_int();\ 168 /* LDV_COMMENT_OTHER If lock is free choose arbitrary action*/\ 169 if(ldv_lock_TEMPLATE==1 && is_lock_held_by_another_thread)\ 170 {\ 171 /* LDV_COMMENT_CHANGE_STATE Goto locked state*/\ 172 ldv_lock_TEMPLATE=2;\ 173 /* LDV_COMMENT_RETURN The lock is acquired*/\ 174 return 1;\ 175 }\ 176 else\ 177 {\ 178 /* LDV_COMMENT_RETURN The lock is not acquired*/\ 179 return 0;\ 180 }\ 181 } while(0) 182 183 #define __ldv_spin_checklocked(free,busy) \ 184 do {\ 185 int is_lock_held_by_another_thread;\ 186 /* LDV_COMMENT_OTHER Construct an arbitrary flag*/\ 187 is_lock_held_by_another_thread = ldv_undef_int();\ 188 /* LDV_COMMENT_OTHER If lock is free choose arbitrary action*/\ 189 if(ldv_lock_TEMPLATE==1 && is_lock_held_by_another_thread)\ 190 {\ 191 /* LDV_COMMENT_RETURN The lock is free*/\ 192 return free;\ 193 }\ 194 else\ 195 {\ 196 /* LDV_COMMENT_RETURN The lock is not free*/\ 197 return busy;\ 198 }\ 199 } while(0) 200 201 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_lock_irqsave(?!_nested)') Acquires the lock and checks for double spin lock*/ 202 void ldv_spin_lock_irqsave_TEMPLATE(spinlock_t *lock, unsigned long flags) { 203 __ldv_spin_lock(); 204 } 205 206 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_lock_nested') Acquires the lock and checks for double spin lock*/ 207 void ldv_spin_lock_nested_TEMPLATE(spinlock_t *lock, int subclass) { 208 __ldv_spin_lock(); 209 } 210 211 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_lock_nest_lock') Acquires the lock and checks for double spin lock*/ 212 void ldv_spin_lock_nest_lock_TEMPLATE(spinlock_t *lock, void *map) { 213 __ldv_spin_lock(); 214 } 215 216 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_lock_irqsave_nested') Acquires the lock and checks for double spin lock*/ 217 void ldv_spin_lock_irqsave_nested_TEMPLATE(spinlock_t *lock, unsigned long flags, int subclass) { 218 __ldv_spin_lock(); 219 } 220 221 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_trylock_irqsave(?!_nested)') Tryies to acquire the lock and returns one if successful*/ 222 int ldv_spin_trylock_irqsave_TEMPLATE(spinlock_t *lock, unsigned long flags) { 223 __ldv_spin_trylock(); 224 } 225 226 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_lock(?!_bh|_irq|_irqsave|_nested|_irqsave_nested|_nest_lock)') Acquires the lock and checks for double spin lock*/ 227 void ldv_spin_lock_TEMPLATE(spinlock_t *lock) { 228 __ldv_spin_lock(); 229 } 230 231 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_lock_bh') Acquires the lock and checks for double spin lock*/ 232 void ldv_spin_lock_bh_TEMPLATE(spinlock_t *lock) { 233 __ldv_spin_lock(); 234 } 235 236 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_lock_irq(?!save|save_nested)') Acquires the lock and checks for double spin lock*/ 237 void ldv_spin_lock_irq_TEMPLATE(spinlock_t *lock) { 238 __ldv_spin_lock(); 239 } 240 241 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_trylock(?!_bh|_irq|_irqsave|_irqsave_nested)') Tryies to acquire the lock and returns one if successful*/ 242 int ldv_spin_trylock_TEMPLATE(spinlock_t *lock) { 243 __ldv_spin_trylock(); 244 } 245 246 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_trylock_bh') Tryies to acquire the lock and returns one if successful*/ 247 int ldv_spin_trylock_bh_TEMPLATE(spinlock_t *lock) { 248 __ldv_spin_trylock(); 249 } 250 251 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_trylock_irq(?!save|save_nested)') Tryies to acquire the lock and returns one if successful*/ 252 int ldv_spin_trylock_irq_TEMPLATE(spinlock_t *lock) { 253 __ldv_spin_trylock(); 254 } 255 256 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_unlock(?!_bh|_irq|_irqrestore)') Releases the lock and checks that lock was acquired before*/ 257 void ldv_spin_unlock_TEMPLATE(spinlock_t *lock) { 258 __ldv_spin_unlock(); 259 } 260 261 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_unlock_bh') Releases the lock and checks that lock was acquired before*/ 262 void ldv_spin_unlock_bh_TEMPLATE(spinlock_t *lock) { 263 __ldv_spin_unlock(); 264 } 265 266 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_unlock_irq(?!restore)') Releases the lock and checks that lock was acquired before*/ 267 void ldv_spin_unlock_irq_TEMPLATE(spinlock_t *lock) { 268 __ldv_spin_unlock(); 269 } 270 271 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_unlock_irqrestore') Releases the lock and checks that lock was acquired before*/ 272 void ldv_spin_unlock_irqrestore_TEMPLATE(spinlock_t *lock, unsigned long flags) { 273 __ldv_spin_unlock(); 274 } 275 276 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_unlock_wait') If the some process is holding the lock then it waits until it will be released*/ 277 void ldv_spin_unlock_wait_TEMPLATE(spinlock_t *lock) { 278 /* LDV_COMMENT_ASSERT The spinlock must not be locked by the current process*/ 279 ldv_assert(ldv_lock_TEMPLATE==1); 280 } 281 282 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_is_locked') Checks whether the lock is free or not*/ 283 int ldv_spin_is_locked_TEMPLATE(spinlock_t *lock) { 284 __ldv_spin_checklocked(0,1); 285 } 286 287 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_is_contended')*/ 288 int ldv_spin_is_contended_TEMPLATE(spinlock_t *lock) { 289 int is_lock_contended; 290 /* LDV_COMMENT_OTHER Construct an arbitrary flag*/ 291 is_lock_contended = ldv_undef_int(); 292 /* LDV_COMMENT_OTHER Choose arbitrary action*/ 293 if(is_lock_contended) 294 { 295 /* LDV_COMMENT_RETURN The lock is contended*/ 296 return 1; 297 } 298 else 299 { 300 /* LDV_COMMENT_RETURN The lock is not contended*/ 301 return 0; 302 } 303 } 304 305 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_spin_can_lock') Checks whether the lock is free or not*/ 306 int ldv_spin_can_lock_TEMPLATE(spinlock_t *lock) { 307 __ldv_spin_checklocked(1,0); 308 } 309 310 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_atomic_dec_and_lock') Locks on reaching reference count zero*/ 311 int ldv_atomic_dec_and_lock_TEMPLATE(spinlock_t *lock, atomic_t *atomic) { 312 int is_atomic_counter_is_one; 313 /* LDV_COMMENT_OTHER Construct an arbitrary flag*/ 314 is_atomic_counter_is_one = ldv_undef_int(); 315 /* LDV_COMMENT_OTHER Choose arbitrary action*/ 316 if(is_atomic_counter_is_one) { 317 /* LDV_COMMENT_RETURN Set counter to zero*/ 318 atomic_dec(atomic); 319 /* LDV_COMMENT_RETURN Acquire the lock and return true*/ 320 __ldv_spin_lock(); 321 return 1; 322 } else { 323 /* LDV_COMMENT_RETURN Return false*/ 324 return 0; 325 } 326 } 327 328 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_check_final_state') Check that the spinlock is unlocked at the end*/ 329 void ldv_check_final_state_TEMPLATE(void) 330 { 331 /* LDV_COMMENT_ASSERT The spinlock must be unlocked at the end*/ 332 ldv_assert(ldv_lock_TEMPLATE == 1); 333 } 334 335 /* LDV_COMMENT_MODEL_FUNCTION_DEFINITION(name='ldv_initialize') Initialize spinlock variables*/ 336 void ldv_initialize_TEMPLATE(void) 337 { 338 /* LDV_COMMENT_ASSERT Initialize spinlock with initial model value*/ 339 ldv_lock_TEMPLATE = 1; 340 }

Here is the explanation of the rule violation arisen in your driver for the corresponding kernel.

Note that there may be no error indeed. Please see on error trace and source code to understand whether there is an error in your driver.

The Error trace column contains the path on which rule is violated. You can choose some entity classes to be shown or hiden by clicking on the corresponding checkboxes or in the advanced Others menu. Also you can show or hide each particular entity by clicking on the corresponding - or +. In hovering on some entities you can see their descriptions and meaning. Also the error trace is binded with the source code. Line numbers are shown as links on the left. You can click on them to open the corresponding line in source code. Line numbers and file names are shown in entity descriptions.

The Source code column contains content of files related with the error trace. There are your driver (note that there are some our modifications at the end), kernel headers and rule source code. Tabs show the currently opened file and other available files. In hovering you can see file names in titles. On clicking the corresponding file content will be shown.