diff options
Diffstat (limited to 'chapters/schedule.tex')
| -rw-r--r-- | chapters/schedule.tex | 2 |
1 files changed, 1 insertions, 1 deletions
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. |