Síntesis y verificación de controladores de dispositivo
Los controladores de dispositivos son programas que permiten que el software o los programas informáticos de nivel superior interactúen con un dispositivo de hardware . Estos componentes de software actúan como un enlace entre los dispositivos y los sistemas operativos , comunicándose con cada uno de estos sistemas y ejecutando comandos. Proporcionan una capa de abstracción para el software anterior y también median la comunicación entre el kernel del sistema operativo y los dispositivos siguientes.
Por lo general, los sistemas operativos son compatibles con los controladores de dispositivos comunes y, por lo general, los proveedores de hardware proporcionan el controlador de dispositivo para sus dispositivos de hardware para la mayoría de las plataformas. El escalado agresivo de los dispositivos de hardware y los componentes de software complejos ha hecho que el proceso de desarrollo de controladores de dispositivos sea engorroso y complejo. Cuando el tamaño y la funcionalidad de los controladores comenzaron a aumentar, los controladores de dispositivos se convirtieron en un factor clave para definir la confiabilidad del sistema. Esto ha creado un incentivo hacia la síntesis y verificación automáticas de controladores de dispositivos. Este artículo arroja algo de luz sobre algunos enfoques de síntesis y verificación de controladores de dispositivos.
Los controladores de dispositivos son el principal componente defectuoso en la mayoría de los sistemas. El proyecto Berkeley Open Infrastructure for Network Computing (BOINC) descubrió que los bloqueos del sistema operativo se deben principalmente a un código de controlador de dispositivo mal escrito. [1] En Windows XP , los controladores representan el 85% de las fallas informadas. En el kernel de Linux 2.4.1, el código del controlador de dispositivo representa aproximadamente el 70% del tamaño del código. [2] La falla del controlador puede bloquear todo el sistema mientras se ejecuta en el modo kernel. Estos hallazgos dieron como resultado varias metodologías y técnicas para la verificación de controladores de dispositivos. Una alternativa fue desarrollar técnicas que puedan sintetizar controladores de dispositivos de manera robusta. Una menor interacción humana en el proceso de desarrollo y la especificación adecuada del dispositivo y los sistemas operativos pueden conducir a controladores más confiables.
La otra motivación para la síntesis de controladores es la gran cantidad de combinaciones de sistemas operativos y dispositivos. Cada uno de ellos tiene su propio conjunto de control y especificaciones de entrada / salida, lo que dificulta el soporte de dispositivos de hardware en cada uno de los sistemas operativos. Por tanto, la capacidad de utilizar un dispositivo con un sistema operativo requiere la disponibilidad de la combinación de controladores de dispositivo correspondiente. Los proveedores de hardware generalmente proporcionan los controladores para Windows, Linux y Mac OS, pero debido a los altos costos de desarrollo o transferencia y las dificultades de soporte técnico , no pueden proporcionar controladores en todas las plataformas. Una técnica de síntesis automatizada puede ayudar a los proveedores a proporcionar controladores que admitan cualquier dispositivo en cualquier sistema operativo.
La ola de verificación de controladores de dispositivos fue iniciada por Microsoft a través de su proyecto SLAM ya en el año 2000. La motivación para el proyecto fue que se descubrió que 500,000 choques reportados por día fueron causados por un controlador de video, lo que generó preocupación sobre el gran vulnerabilidad en el uso de controladores de dispositivos complejos. Se pueden encontrar más detalles aquí , en el discurso pronunciado por Bill Gates. Desde entonces, se han propuesto una gran cantidad de técnicas estáticas y en tiempo de ejecución para la detección y el aislamiento de errores.
