Uso de Haskell para sistemas de tiempo real de gran tamaño: ¿cómo (si?)?

Question

He tenido curiosidad por comprender si es posible aplicar el poder de Haskell al mundo embebido en tiempo real, y en Google he encontrado el paquete Atom. Supongo que en el caso complejo, el código podría tener todos los errores C clásicos: bloqueos, daños en la memoria, etc., que luego tendría que rastrearse hasta el código Haskell original que los causó . Entonces, esta es la primera parte de la pregunta: "Si tuviste la experiencia con Atom, ¿cómo lidiaste con la tarea de depurar los errores de bajo nivel en el código C compilado y corregirlos en el código original de Haskell?"

He buscado algunos ejemplos más para Atom, this blog post menciona el código C resultante 22KLOC (y obviamente no hay código :), el included example es un juguete. This y this referencias tienen un código un poco más práctico, pero aquí es donde esto termina. Y la razón por la que puse "considerable" en el tema es, estoy más interesado si puede compartir sus experiencias de trabajo con el código C generado en el rango de 300KLOC +.

Como soy un novato en Haskell, obviamente puede haber otras formas que no encontré debido a mis incógnitas desconocidas, por lo que cualquier otro puntero para la autoeducación en esta área sería muy apreciado, y esta es la segunda parte de la pregunta: "¿Cuáles serían algunos otros métodos prácticos (si) de hacer un desarrollo en tiempo real en Haskell?". Si el multinúcleo también está en la imagen, eso es un plus extra :-)

(Sobre el uso de Haskell para este propósito: por lo que leo en this blog post, la recolección de basura y la pereza en Haskell lo hace un horario no determinista- sabia, pero tal vez en dos años algo ha cambiado Real world Haskell programming pregunta sobre SO era el más cercano que pude encontrar a este tema)

Nota:. "en tiempo real" anterior es que sería más cerca de "tiempo real duro" - Tengo curiosidad si es posible garantizar que el tiempo de pausa cuando la tarea principal no se está ejecutando sea menor a 0.5 ms.

Answer 1

En Galois utilizamos Haskell por dos cosas:

• tiempo real suave (capas de dispositivos del sistema operativo, redes), donde los tiempos de respuesta de 1-5 ms son plausibles. GHC genera código rápido, y tiene mucho soporte para ajustar el GC y el programador para obtener los tiempos correctos.
• para verdaderos sistemas en tiempo real Los EDSL se usan para generar código para otros lenguajes que proporcionan garantías de tiempo más fuertes. P.ej. Cryptol, Atom y Copilot.

Tenga cuidado de distinguir el EDSL (copiloto o átomo) del idioma de host (Haskell).

---

Algunos ejemplos de sistemas críticos, y en algunos casos, los sistemas en tiempo real, ya sea escrito o generado a partir de Haskell, producido por Galois.

EDSLs

• Copilot: A Hard Real-Time Runtime Monitor - un DSL para aviónica monitoreo en tiempo real
• Equivalence and Safety Checking in Cryptol - un DSL para componentes criptográficos de sistemas críticos

Sistemas

• HaLVM - un micronúcleo ligero para aplicaciones embebidas y móviles
• TSE - un dispositivo de dominios cruzados (nivel de seguridad) a la red

Answer 2

Pasará mucho tiempo antes de que exista un sistema Haskell que se ajuste a la memoria pequeña y pueda garantizar tiempos de pausa inferiores a milisegundos. La comunidad de implementadores Haskell simplemente no parece estar interesada en este tipo de objetivo.

Existe un gran interés en usar Haskell o algo parecido a Haskell para compilar algo muy eficiente; por ejemplo, Bluespec compila al hardware.

No creo que satisfaga sus necesidades, pero si está interesado en la programación funcional y los sistemas integrados, debe aprender acerca de Erlang.

Answer 3

No creo que Haskell u otros lenguajes recogidos de basura sean adecuados para sistemas en tiempo real, ya que los GC tienden a amortizar sus tiempos de ejecución en breves pausas.

Escribir en Atom no es exactamente programación en Haskell, ya que aquí Haskell puede verse como un simple preprocesador del programa que está escribiendo.

creo Haskell es un preprocesador impresionante, y el uso de DSEL como Atom es probablemente una gran manera de crear sistemas de tiempo real duro de tamaño considerable, pero no sé si Atom ajusta a la ley o no. Si no lo hace, estoy bastante seguro de que es posible (¡y animo a cualquiera que lo haga!) A implementar un DSEL que sí lo haga.

Tener un preprocesador muy fuerte como Haskell para un lenguaje de bajo nivel abre una gran oportunidad para implementar abstracciones a través de la generación de código que son mucho más torpes cuando se implementan como generadores de texto en código C.

Answer 4

Andrew,

Sí, puede ser difícil de depurar problemas a través del código generado de regreso a la fuente original. Una cosa que ofrece Atom es un medio para sondear las expresiones internas, luego deja al usuario la tarea de manejar estas sondas. Para la prueba de vehículos, construimos un transmisor (en Atom) y transmitimos las sondas a través de un bus CAN. Luego, podemos capturar estos datos, formatearlos y luego verlos con herramientas como GTKWave, ya sea en postprocesamiento o en tiempo real. Para la simulación de software, las sondas se manejan de manera diferente. En lugar de obtener datos de sonda de un protocolo CAN, se crean ganchos en el código C para levantar los valores de la sonda directamente. Los valores de la sonda se usan luego en el marco de prueba de la unidad (distribuido con Atom) para determinar si una prueba pasa o no y para calcular la cobertura de la simulación.

Answer 5

He estado jugando con Atom. Es genial, pero creo que es mejor para sistemas pequeños. Sí, se ejecuta en camiones y autobuses e implementa aplicaciones críticas del mundo real, pero eso no significa que esas aplicaciones sean necesariamente grandes o complejas. Realmente es para aplicaciones duras en tiempo real y hace todo lo posible para que cada operación tome la misma cantidad de tiempo. Por ejemplo, en lugar de una instrucción if/else que ejecuta condicionalmente una de las dos ramas de código que pueden diferir en el tiempo de ejecución, tiene una instrucción "mux" que siempre ejecuta ambas ramas antes de seleccionar condicionalmente uno de los dos valores calculados (por lo que el total el tiempo de ejecución es el mismo cualquiera que sea el valor seleccionado). No tiene ningún tipo de sistema significativo aparte de los tipos incorporados (comparables a los C) que se aplican a través de los valores GADT pasados ​​a través de la mónada Atom. El autor está trabajando en una herramienta de verificación estática que analiza el código de salida C, que es bastante bueno (utiliza un solucionador de SMT), pero creo que Atom se beneficiaría de más funciones y controles de nivel de fuente.Incluso en mi aplicación de tamaño de juguete (controlador de linterna LED), he cometido una serie de errores de novato que alguien con más experiencia con el paquete podría evitar, pero que dieron como resultado un código de salida defectuoso que preferiría haber sido capturado por el compilador en lugar de a través de pruebas. Por otro lado, todavía está en la versión 0.1. Algo por lo que las mejoras sin duda vendrán.