rdp->count++; /* *  Should we directly call rcu_do_batch() here ? *  if (unlikely(rdp->count > 10000)) *      rcu_do_batch(rdp); */ 
void fastcall call_rcu_bh(struct rcu_head *head,				void (*func)(struct rcu_head *rcu)){	unsigned long flags;	struct rcu_data *rdp;	head->func = func;	head->next = NULL;	local_irq_save(flags);	rdp = &__get_cpu_var(rcu_bh_data);	*rdp->nxttail = head;	rdp->nxttail = &head->next;	local_irq_restore(flags);}
4520	/local/tlutelli/issta_data/temp/c/2005_temp/2005/4520/5ee832dbc6770135ec8d63296af0a4374557bb79/rcupdate.c/buggy/kernel/rcupdate.c