Index: /soft/giet_vm/giet_drivers/bdv_driver.c
===================================================================
--- /soft/giet_vm/giet_drivers/bdv_driver.c	(revision 468)
+++ /soft/giet_vm/giet_drivers/bdv_driver.c	(revision 469)
@@ -97,5 +97,5 @@
 
     // get the lock protecting BDV
-    _lock_acquire( &_bdv_lock );
+    _spin_lock_acquire( &_bdv_lock );
 
 #if GIET_DEBUG_IOC_DRIVER
@@ -159,5 +159,5 @@
 
         // release lock
-        _lock_release( &_bdv_lock );      
+        _spin_lock_release( &_bdv_lock );      
     }
     // in USER or KERNEL mode, we deschedule the task.
@@ -220,5 +220,5 @@
         // reset _bdv_status and release lock
         _bdv_status = BLOCK_DEVICE_IDLE; 
-        _lock_release( &_bdv_lock );      
+        _spin_lock_release( &_bdv_lock );      
     }
 
Index: /soft/giet_vm/giet_drivers/tty_driver.c
===================================================================
--- /soft/giet_vm/giet_drivers/tty_driver.c	(revision 468)
+++ /soft/giet_vm/giet_drivers/tty_driver.c	(revision 469)
@@ -17,21 +17,4 @@
 # error: You must define SEG_TTY_BASE in the hard_config.h file
 #endif
-
-#if !defined(NB_TTY_CHANNELS)
-# error: You must define NB_TTY_CHANNELS in the hard_config.h file
-#endif
-
-#if (NB_TTY_CHANNELS == 0)
-# error: The NB_TTY_CHANNELS in the hard_config.h file cannot be 0
-#endif
-
-////////////////////////////////////////////////////////////////////////////////////
-//               global variables
-////////////////////////////////////////////////////////////////////////////////////
-
-simple_lock_t  _tty_tx_lock[NB_TTY_CHANNELS] __attribute__((aligned(64)));
-
-unsigned int   _tty_rx_buf[NB_TTY_CHANNELS];
-unsigned int   _tty_rx_full[NB_TTY_CHANNELS]; 
 
 ////////////////////////////////////////////////////////////////////////////////////
Index: /soft/giet_vm/giet_drivers/tty_driver.h
===================================================================
--- /soft/giet_vm/giet_drivers/tty_driver.h	(revision 468)
+++ /soft/giet_vm/giet_drivers/tty_driver.h	(revision 469)
@@ -24,4 +24,5 @@
 #define _GIET_TTY_DRIVERS_H_
 
+#include "hard_config.h"
 #include "locks.h"
 
@@ -41,11 +42,12 @@
 
 ////////////////////////////////////////////////////////////////////////////////////
-//               global variables
+//                   global variables
+// These variables must be defined both in boot code and in kernel_init code.
 ////////////////////////////////////////////////////////////////////////////////////
 
-extern simple_lock_t  _tty_tx_lock[];
+extern sbt_lock_t     _tty_tx_lock[NB_TTY_CHANNELS];
 
-extern unsigned int   _tty_rx_buf[];
-extern unsigned int   _tty_rx_full[]; 
+extern unsigned int   _tty_rx_buf[NB_TTY_CHANNELS];
+extern unsigned int   _tty_rx_full[NB_TTY_CHANNELS]; 
 
 //////////////////////////////////////////////////////////////////////////////////