El investigador predoctoral del Instituto IMDEA Software, Pepe Vila, participó en RootedCON 2020 el pasado día 7 de marzo y dio una charla titulada: “Los 80 nunca murieron: teoría autómata para revertir CPUs modernas” (ver presentación). Su ponencia se basa en el resultado de investigación que se materializó en la publicación ‘CacheQuery: Learning Replacement Policies from Hardware Caches’ que elaboró con el apoyo y respaldo de los investigadores Pierre Ganty y Marco Guarnieri, del Instituto IMDEA Software, y Boris Köpf, de Microsoft Research. Esta investigación desvela la implementación, previamente desconocida, de las políticas de reemplazo de caché utilizadas en procesadores modernos.
Comprender el comportamiento temporal de las CPUs modernas es crucial para optimizar el código y asegurar propiedades de seguridad críticas. Desafortunadamente, el comportamiento temporal de los procesadores modernos depende de detalles muy sutiles y poco documentados de su microarquitectura, lo que desencadena esfuerzos laboriosos de ingeniería inversa. Las políticas de reemplazamiento de cachés han recibido una atención especial, porque controlan el contenido almacenado en la jerarquía de la memoria y, por lo tanto, influyen en gran medida en el tiempo de ejecución.
En la publicación, que ha sido aceptada en PLDI'20 (Conference on Programming Language Design and Implementation), los investigadores del Instituto IMDEA Software y Microsoft Research presentan una solución de extremo a extremo para aprender automáticamente las políticas de reemplazo de caché a partir de mediciones de tiempo en el hardware. Su aportación se basa en dos contribuciones principales: una herramienta, llamada CacheQuery, que proporciona una interfaz para cualquier conjunto en la jerarquía de cachés, liberando al usuario de tener que lidiar con detalles intrincados como la traducción de direcciones, el mapeo de índices, la interferencia de otros niveles de caché o el ruido de las mediciones; y, un algoritmo, llamado Polca, que proporciona un autómata abstracto para la política de reemplazo de cachés, y explota varias simetrías que hacen que las técnicas de aprendizaje de autómatas sean aplicables al problema. Además, han sido capaces de sintetizar programas para derivar automáticamente descripciones legibles de la política de reemplazo aprendida.
En la fase experimental, sus pruebas han sido exitosas en el aprendizaje de varias políticas de reemplazo de caché utilizadas en los procesadores mas recientes de Intel, incluyendo dos políticas no documentadas anteriormente.
