From 5432fc846a60bf6b2567cd5d1f886de052e34940 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Mon, 18 Apr 2022 16:23:37 +0100 Subject: More work on all chapters --- chapters/schedule.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'chapters/schedule.tex') diff --git a/chapters/schedule.tex b/chapters/schedule.tex index 49d5251..bf62c59 100644 --- a/chapters/schedule.tex +++ b/chapters/schedule.tex @@ -42,7 +42,7 @@ proof. Vericert to pass through \SSA, as well as GSA, and finally generate dynamic HTL (or some other similar hardware language). During my visit at Inria Rennes, I worked with Sandrine Blazy and Delphine Demange to extend CompCertSSA~\cite[barthe14_formal_verif_ssa_based_middl_end_compc] with -\infull{GSA} (\GSA)~\cite[ottenstein90_progr_depen_web]. Not only should this allow for global +\GSA~\cite[ottenstein90_progr_depen_web]. Not only should this allow for global optimisations of \SSA\ code, but it should also allow for a more straightforward translation to hardware as the GSA code can just be viewed as a \DFG. Instead of working on modulo scheduling, it could therefore be interesting to work on a formally verified dynamic scheduling translation. -- cgit