__thread / _Thread_local

[monniaux]

C11 defines the _Thread_local keyword, and GCC has long had the __thread modifier.
They define data to reside in the thread-local storage. Basically, if x is thread-local, then it behaves as a separate variable depending on the thread where its address is taken (either explicitly with & or implicitly when used as an lvalue or expr).

CompCert does not support multi-threading. However, on some platforms, the system libraries put essential data (including stdin, stdout, stderr) in thread-local storage, meaning that code compiled with vanilla CompCert cannot do fprintf(stderr, ...) (one gets a linkage error for referring to a thread-local object using a normal relocation).

As far as I understand CompCert internals, only the symbol name is transmitted to the back-end when a “load symbol” opcode is generated. Maybe it would be interesting to be able to convey some attributes, such as whether the symbol is marked as thread-local, to the back-end, along with the symbol name, so that it is possible to implement such references.

(I realize that this is probably a lot of work for a little problem.)

[bschommer]

I think this can be done and the changes would mostly affect the frontend as well as the code emitter, adding the enhancement label.

[monniaux]

Thank you. I currently work around this by testing syntactically for the name of some known thread local global variable defined in libc in the function emitting the assembly code for "load symbol" in the backend backend, and emitting a special instruction sequence in this case.

[monniaux]

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 24e3cacf..d03392b1 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -45,16 +45,29 @@ let decl_atom : (AST.ident, atom_info) Hashtbl.t = Hashtbl.create 103
 
 let atom_is_static a =
   try
-    (Hashtbl.find decl_atom a).a_storage = C.Storage_static
+    match (Hashtbl.find decl_atom a).a_storage with
+    | C.Storage_static | C.Storage_thread_local_static -> true
+    | _ -> false
   with Not_found ->
     false
 
 let atom_is_extern a =
   try
-    (Hashtbl.find decl_atom a).a_storage = C.Storage_extern
+    match (Hashtbl.find decl_atom a).a_storage with
+    | C.Storage_extern| C.Storage_thread_local_extern -> true
+    | _ -> false
   with Not_found ->
     false
 
+let atom_is_thread_local a =
+  try
+    match (Hashtbl.find decl_atom a).a_storage with
+    | C.Storage_thread_local_extern| C.Storage_thread_local_static
+    | C.Storage_thread_local -> true
+    | _ -> false
+  with Not_found ->
+    false
+  
 let atom_alignof a =
   try
     (Hashtbl.find decl_atom a).a_alignment
@@ -1226,7 +1239,8 @@ let convertFundef loc env fd =
   let vars =
     List.map
       (fun (sto, id, ty, init) ->
-        if sto = Storage_extern || sto = Storage_static then
+        if   sto = Storage_extern || sto = Storage_thread_local_extern
+          || sto = Storage_static || sto = Storage_thread_local_static then
           unsupported "'static' or 'extern' local variable";
         if init <> None then
           unsupported "initialized local variable";
@@ -1328,7 +1342,8 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
   let init' =
     match optinit with
     | None ->
-        if sto = C.Storage_extern then [] else [AST.Init_space sz]
+       if sto = C.Storage_extern || sto = C.Storage_thread_local_extern
+       then [] else [AST.Init_space sz]
     | Some i ->
         convertInitializer env ty i in
   let (section, access) =
@@ -1336,7 +1351,8 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
   if Z.gt sz (Z.of_uint64 0xFFFF_FFFFL) then
     error "'%s' is too big (%s bytes)"
                    id.name (Z.to_string sz);
-  if sto <> C.Storage_extern && Cutil.incomplete_type env ty then
+  if sto <> C.Storage_extern && sto <> C.Storage_thread_local_extern
+     && Cutil.incomplete_type env ty then
     error "'%s' has incomplete type" id.name;
   Hashtbl.add decl_atom id'
     { a_storage = sto;
@@ -1434,7 +1450,7 @@ let cleanupGlobals p =
         if IdentSet.mem fd.fd_name !strong then
           error "multiple definitions of %s" fd.fd_name.name;
         strong := IdentSet.add fd.fd_name !strong
-    | C.Gdecl(Storage_extern, id, ty, init) ->
+    | C.Gdecl((Storage_extern|Storage_thread_local_extern), id, ty, init) ->
         extern := IdentSet.add id !extern
     | C.Gdecl(sto, id, ty, Some i) ->
         if IdentSet.mem id !strong then
@@ -1453,7 +1469,7 @@ let cleanupGlobals p =
         match g.gdesc with
         | C.Gdecl(sto, id, ty, init) ->
             let better_def_exists =
-              if sto = Storage_extern then
+              if sto = Storage_extern || sto = Storage_thread_local_extern then
                 IdentSet.mem id !strong || IdentSet.mem id !weak
               else if init = None then
                 IdentSet.mem id !strong
diff --git a/cparser/C.mli b/cparser/C.mli
index 15717565..3c271f3f 100644
--- a/cparser/C.mli
+++ b/cparser/C.mli
@@ -86,8 +86,11 @@ type attributes = attribute list
 
 type storage =
   | Storage_default (* used for toplevel names without explicit storage *)
+  | Storage_thread_local
   | Storage_extern
   | Storage_static
+  | Storage_thread_local_extern
+  | Storage_thread_local_static
   | Storage_auto    (* used for block-scoped names without explicit storage *)
   | Storage_register
 
diff --git a/cparser/Cabs.v b/cparser/Cabs.v
index 5f12e8a1..2dae061a 100644
--- a/cparser/Cabs.v
+++ b/cparser/Cabs.v
@@ -54,7 +54,7 @@ Inductive typeSpecifier := (* Merge all specifiers into one type *)
   | Tenum : option string -> option (list (string * option expression * loc)) -> list attribute -> typeSpecifier
 
 with storage :=
-  AUTO | STATIC | EXTERN | REGISTER | TYPEDEF
+  AUTO | STATIC | EXTERN | REGISTER | TYPEDEF | THREAD_LOCAL
 
 with cvspec :=
 | CV_CONST | CV_VOLATILE | CV_RESTRICT
diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index ecf83779..7bae2fe2 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -354,7 +354,9 @@ and is_constant_lval env e =
       begin match Env.find_ident env id with
       | Env.II_ident(sto, _) ->
           begin match sto with
-          | Storage_default | Storage_extern | Storage_static -> true
+          | Storage_default | Storage_extern | Storage_static
+          | Storage_thread_local | Storage_thread_local_extern | Storage_thread_local_static
+            -> true
           | Storage_auto | Storage_register -> false
           end
       | Env.II_enum _ -> false   (* should not happen *)
diff --git a/cparser/Cleanup.ml b/cparser/Cleanup.ml
index 63ac8ac1..9f19395a 100644
--- a/cparser/Cleanup.ml
+++ b/cparser/Cleanup.ml
@@ -126,14 +126,14 @@ let add_enum e =
 *)
 
 let visible_decl (sto, id, ty, init) =
-  sto = Storage_default &&
+  (sto = Storage_default || sto = Storage_thread_local) &&
   match ty with TFun _ -> false | _ -> true
 
 let visible_fundef f =
   match f.fd_storage with
-  | Storage_default -> not f.fd_inline
-  | Storage_extern -> true
-  | Storage_static -> false
+  | Storage_default | Storage_thread_local -> not f.fd_inline
+  | Storage_extern | Storage_thread_local_extern -> true
+  | Storage_static | Storage_thread_local_static -> false
   | Storage_auto | Storage_register -> assert false
 
 let rec add_init_globdecls accu = function
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 9aeec421..78970990 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -361,6 +361,9 @@ let storage pp = function
   | Storage_default -> ()
   | Storage_extern -> fprintf pp "extern "
   | Storage_static -> fprintf pp "static "
+  | Storage_thread_local -> fprintf pp "_Thread_local"
+  | Storage_thread_local_extern -> fprintf pp "extern _Thread_local"
+  | Storage_thread_local_static -> fprintf pp "static _Thread_local"
   | Storage_auto -> ()   (* used only in blocks, where it can be omitted *)
   | Storage_register -> fprintf pp "register "
 
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 3dbb9d45..3c754dd6 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -152,6 +152,9 @@ let name_of_storage_class = function
   | Storage_default -> "<default>"
   | Storage_extern -> "'extern'"
   | Storage_static -> "'static'"
+  | Storage_thread_local -> "'_Thread_local'"
+  | Storage_thread_local_extern -> "'_Thread_local extern'"
+  | Storage_thread_local_static -> "'_Thread_local static'"
   | Storage_auto -> "'auto'"
   | Storage_register -> "'register'"
 
@@ -177,15 +180,29 @@ let combine_toplevel_definitions loc env s old_sto old_ty sto ty =
     | Storage_static,Storage_static
     | Storage_extern,Storage_extern
     | Storage_default,Storage_default -> sto
-    | _,Storage_static ->
+    | Storage_thread_local_static,Storage_thread_local_static
+    | Storage_thread_local_extern,Storage_thread_local_extern
+    | Storage_thread_local,Storage_thread_local -> sto
+    | _,Storage_static | _,Storage_thread_local_static ->
 	error loc "static declaration of '%s' follows non-static declaration" s;
         sto
     | Storage_static,_ -> Storage_static (* Static stays static *)
-    | Storage_extern,_ -> if is_function_type env new_ty then Storage_extern else sto
+    | Storage_thread_local_static,_ -> Storage_thread_local_static (* Thread-local static stays static *)
+    | (Storage_extern|Storage_thread_local_extern),_ -> if is_function_type env new_ty then Storage_extern else sto
     | Storage_default,Storage_extern ->
       if is_global_defined s && is_function_type env ty then
         warning loc Extern_after_definition "this extern declaration follows a non-extern definition and is ignored";
       Storage_extern
+    | Storage_thread_local,Storage_thread_local_extern ->
+      if is_global_defined s && is_function_type env ty then
+        warning loc Extern_after_definition "this extern declaration follows a non-extern definition and is ignored";
+      Storage_extern
+    | Storage_thread_local, Storage_default ->
+       error loc "Non thread-local declaration follows thread-local";
+       sto
+    | Storage_default, (Storage_thread_local|Storage_thread_local_extern) ->
+       error loc "Thread-local declaration follows non thread-local";
+       sto
     | _,Storage_extern -> old_sto
     (* "auto" and "register" don't appear in toplevel definitions.
        Normally this was checked earlier.  Generate error message
@@ -638,13 +655,26 @@ let rec elab_specifier ?(only = false) loc env specifier =
       restrict := cv = CV_RESTRICT;
       attr := add_attributes (elab_cvspec env cv) !attr
   | SpecStorage st ->
-      if !sto <> Storage_default && st <> TYPEDEF then
+      if !sto <> Storage_default && st <> TYPEDEF && st <> THREAD_LOCAL then
         error loc "multiple storage classes in declaration specifier";
       begin match st with
       | AUTO -> sto := Storage_auto
       | STATIC -> sto := Storage_static
       | EXTERN -> sto := Storage_extern
       | REGISTER -> sto := Storage_register
+      | THREAD_LOCAL ->
+         sto := (match !sto with
+                 | Storage_static | Storage_thread_local_static ->
+                    Storage_thread_local_static
+                 | Storage_extern | Storage_thread_local_extern ->
+                    Storage_thread_local_extern
+                 | Storage_default | Storage_thread_local ->
+                    Storage_thread_local
+                 | Storage_auto|Storage_register ->
+                    error loc "_Thread_local on auto or register variable";
+                    !sto
+                )
+
       | TYPEDEF ->
           if !typedef then
             error loc "multiple uses of 'typedef'";
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index 346477b5..2266a874 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -72,6 +72,7 @@ let () =
       ("goto", fun loc -> GOTO loc);
       ("if", fun loc -> IF loc);
       ("inline", fun loc -> INLINE loc);
+      ("_Thread_local", fun loc -> THREAD_LOCAL loc);
       ("_Noreturn", fun loc -> NORETURN loc);
       ("int", fun loc -> INT loc);
       ("long", fun loc -> LONG loc);
@@ -542,6 +543,7 @@ and singleline_comment = parse
       | Pre_parser.IF loc -> loop (Parser.IF_ loc)
       | Pre_parser.INC loc -> loop (Parser.INC loc)
       | Pre_parser.INLINE loc -> loop (Parser.INLINE loc)
+      | Pre_parser.THREAD_LOCAL loc -> loop (Parser.THREAD_LOCAL loc)
       | Pre_parser.INT loc -> loop (Parser.INT loc)
       | Pre_parser.LBRACE loc -> loop (Parser.LBRACE loc)
       | Pre_parser.LBRACK loc -> loop (Parser.LBRACK loc)
diff --git a/cparser/Parser.vy b/cparser/Parser.vy
index 03bfa590..4f3b9789 100644
--- a/cparser/Parser.vy
+++ b/cparser/Parser.vy
@@ -32,7 +32,7 @@ Require Cabs.
   LEFT_ASSIGN RIGHT_ASSIGN AND_ASSIGN XOR_ASSIGN OR_ASSIGN
 
 %token<Cabs.loc> LPAREN RPAREN LBRACK RBRACK LBRACE RBRACE DOT COMMA
-  SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT AUTO REGISTER INLINE
+  SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT AUTO REGISTER INLINE THREAD_LOCAL
   NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE CONST VOLATILE VOID
   STRUCT UNION ENUM UNDERSCORE_BOOL PACKED ALIGNAS ATTRIBUTE ASM
 
@@ -397,6 +397,8 @@ storage_class_specifier:
     { (Cabs.AUTO, loc) }
 | loc = REGISTER
     { (Cabs.REGISTER, loc) }
+| loc = THREAD_LOCAL
+    { (Cabs.THREAD_LOCAL, loc) }
 
 (* 6.7.2 *)
 type_specifier:
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index 64412194..aeeb9326 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -257,13 +257,16 @@ let rec reserve_public env = function
         match dcl.gdesc with
         | Gdecl(sto, id, _, _) ->
             begin match sto with
-            | Storage_default | Storage_extern -> enter_public env id
+            | Storage_default  | Storage_thread_local
+            | Storage_extern   | Storage_thread_local_extern ->
+               enter_public env id
             | Storage_static -> env
             | _ -> assert false
             end
         | Gfundef f ->
             begin match f.fd_storage with
-            | Storage_default | Storage_extern -> enter_public env f.fd_name
+            | Storage_default | Storage_extern
+              -> enter_public env f.fd_name
             | Storage_static -> env
             | _ -> assert false
             end
diff --git a/cparser/deLexer.ml b/cparser/deLexer.ml
index de0e9b6e..43c1a679 100644
--- a/cparser/deLexer.ml
+++ b/cparser/deLexer.ml
@@ -30,6 +30,7 @@ let delex (symbol : string) : string =
   | "BUILTIN_VA_ARG" -> "__builtin_va_arg"
   | "CONST" -> "const"
   | "INLINE" -> "inline"
+  | "THREAD_LOCAL" -> "_Thread_local"
   | "PACKED" -> "__packed__"
   | "RESTRICT" -> "restrict"
   | "SIGNED" -> "signed"
diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly
index 669ecf5e..e21a3519 100644
--- a/cparser/pre_parser.mly
+++ b/cparser/pre_parser.mly
@@ -54,7 +54,7 @@
   COLON AND MUL_ASSIGN DIV_ASSIGN MOD_ASSIGN ADD_ASSIGN SUB_ASSIGN LEFT_ASSIGN
   RIGHT_ASSIGN AND_ASSIGN XOR_ASSIGN OR_ASSIGN LPAREN RPAREN LBRACK RBRACK
   LBRACE RBRACE DOT COMMA SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT
-  AUTO REGISTER INLINE NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE
+  AUTO REGISTER INLINE THREAD_LOCAL NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE
   UNDERSCORE_BOOL CONST VOLATILE VOID STRUCT UNION ENUM CASE DEFAULT IF ELSE
   SWITCH WHILE DO FOR GOTO CONTINUE BREAK RETURN BUILTIN_VA_ARG ALIGNOF
   ATTRIBUTE ALIGNAS PACKED ASM BUILTIN_OFFSETOF
@@ -430,7 +430,8 @@ storage_class_specifier_no_typedef:
 | STATIC
 | AUTO
 | REGISTER
+| THREAD_LOCAL
     {}
 
 (* [declaration_specifier_no_type] matches declaration specifiers
 

[monniaux]

Currently implemented for KVX in Verimag's versions.