diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index eb06a7c5c..4ef34fe69 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -66,3 +66,5 @@ jobs:
         run: tools/runner.sh test1
       - name: Test alternate configuration
         run: tools/runner.sh test2
+      - name: Test alternate configuration 2
+        run: tools/runner.sh test3
diff --git a/Makefile b/Makefile
index 1e5f0ecaf..6af062c51 100644
--- a/Makefile
+++ b/Makefile
@@ -315,7 +315,7 @@ latexdoc:
 	@chmod a-w $*.v
 
 compcert.ini: Makefile.config
-	(echo "stdlib_path=$(LIBDIR)"; \
+	(echo "stdlib_path=$(RELLIBDIR)"; \
          echo "prepro=$(CPREPRO)"; \
          echo "linker=$(CLINKER)"; \
          echo "asm=$(CASM)"; \
@@ -330,7 +330,8 @@ compcert.ini: Makefile.config
          echo "has_runtime_lib=$(HAS_RUNTIME_LIB)"; \
          echo "has_standard_headers=$(HAS_STANDARD_HEADERS)"; \
          echo "asm_supports_cfi=$(ASM_SUPPORTS_CFI)"; \
-	 echo "response_file_style=$(RESPONSEFILE)";) \
+	 echo "response_file_style=$(RESPONSEFILE)"; \
+	 echo "pic_supported=$(PIC_SUPPORTED)") \
         > compcert.ini
 
 compcert.config: Makefile.config
diff --git a/aarch64/extractionMachdep.v b/aarch64/extractionMachdep.v
index 78eb363fb..143e77e3a 100644
--- a/aarch64/extractionMachdep.v
+++ b/aarch64/extractionMachdep.v
@@ -30,7 +30,7 @@ Extract Constant Archi.abi =>
 Extract Constant SelectOp.symbol_is_relocatable =>
   "match Configuration.system with
     | ""macos"" -> C2C.atom_is_external
-    | _ -> (fun _ -> false)".
+    | _ -> C2C.atom_needs_GOT_access".
 
 (* Asm *)
 
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 4f7363b01..0b20db554 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -52,7 +52,10 @@ let atom_is_static a =
   with Not_found ->
     false
 
-(* Is it possible for symbol [a] to be defined in a DLL? *)
+(* Is it possible for symbol [a] to be defined in a DLL?
+   Yes, unless [a] is defined in the current compilation unit, or is static.
+   (This criterion is appropriate for macOS and for Cygwin; for ELF,
+    see [atom_needs_GOT_access] below.)  *)
 let atom_is_external a =
   match Hashtbl.find decl_atom a with
   | { a_defined = true } -> false
@@ -61,6 +64,20 @@ let atom_is_external a =
   | _ -> true
   | exception Not_found -> true
 
+(* In ELF PIC code, all non-static symbols must be accessed through
+   the GOT, even if they are defined in the current compilation unit.
+   (This is to allow symbol interposition by the dynamic loader.)
+   In ELF PIE code, there is no interposition, so locally-defined
+   symbols do not need GOT access.
+   In non-PIC, non-PIE mode, the GOT is unused. *)
+let atom_needs_GOT_access a =
+  if !Clflags.option_fpic then
+    not (atom_is_static a)
+  else if !Clflags.option_fpie then
+    atom_is_external a
+  else
+    false
+
 let atom_alignof a =
   try
     (Hashtbl.find decl_atom a).a_alignment
diff --git a/configure b/configure
index 9b1102d14..4657cc3ec 100755
--- a/configure
+++ b/configure
@@ -234,6 +234,7 @@ cprepro_options="-E"
 archiver="${toolprefix}ar rcs"
 libmath="-lm"
 responsefile="gnu"
+pic_supported=false
 
 #
 # ARM Target Configuration
@@ -313,9 +314,13 @@ if test "$arch" = "x86" -a "$bitsize" = "32"; then
   case "$target" in
     bsd)
         abi="standard"
+        cc="${toolprefix}cc"
         cc_options="-m32"
+        casm="${toolprefix}cc"
         casm_options="-m32 -c"
+        clinker="${toolprefix}cc"
         clinker_options="-m32"
+        cprepro="${toolprefix}cc"
         cprepro_options="-m32 -U__GNUC__ -E"
         system="bsd"
         ;;
@@ -342,19 +347,27 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
   case "$target" in
     bsd)
         abi="standard"
+        cc="${toolprefix}cc"
         cc_options="-m64"
+        casm="${toolprefix}cc"
         casm_options="-m64 -c"
+        clinker="${toolprefix}cc"
         clinker_options="-m64"
+        clinker_needs_no_pie=false
+        cprepro="${toolprefix}cc"
         cprepro_options="-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"
         system="bsd"
+        pic_supported=true
         ;;
     linux)
         abi="standard"
         cc_options="-m64"
         casm_options="-m64 -c"
         clinker_options="-m64"
+        clinker_needs_no_pie=false
         cprepro_options="-m64 -U__GNUC__ -U__SIZEOF_INT128__ -E"
         system="linux"
+        pic_supported=true
         ;;
     macos|macosx)
         abi="macos"
@@ -365,6 +378,7 @@ if test "$arch" = "x86" -a "$bitsize" = "64"; then
         cprepro_options="-arch x86_64 -U__GNUC__ -U__SIZEOF_INT128__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
         libmath=""
         system="macos"
+        pic_supported=true
         ;;
     cygwin)
         abi="standard"
@@ -395,8 +409,10 @@ if test "$arch" = "riscV"; then
   cc_options="$model_options"
   casm_options="$model_options -c"
   clinker_options="$model_options"
+  clinker_needs_no_pie=false
   cprepro_options="$model_options -U__GNUC__ -E"
   system="linux"
+  pic_supported=true
 fi
 
 #
@@ -407,7 +423,9 @@ if test "$arch" = "aarch64"; then
     linux)
         abi="standard"
         cprepro_options="-U__GNUC__ -E"
-        system="linux";;
+        system="linux"
+        pic_supported=true
+        ;;
     macos|macosx)
         abi="apple"
         casm="${toolprefix}cc"
@@ -419,6 +437,7 @@ if test "$arch" = "aarch64"; then
         cprepro_options="-arch arm64 -U__GNUC__ -U__clang__ -U__BLOCKS__ '-D__attribute__(x)=' '-D__asm(x)=' '-D_Nullable=' '-D_Nonnull=' '-D__DARWIN_OS_INLINE=static inline' -Wno-\\#warnings -E"
         libmath=""
         system="macos"
+        pic_supported=true
         ;;
     *)
         echo "Error: invalid eabi/system '$target' for architecture AArch64." 1>&2
@@ -638,6 +657,15 @@ else
   fi
 fi
 
+#
+# See if $libdir can be accessed with a relative path from $sharedir
+#
+if test "$(dirname "$sharedir")/lib/compcert" = "$libdir"; then
+  rellibdir="../lib/compcert"
+else
+  rellibdir="$libdir"
+fi
+
 #
 # Generate Makefile.config
 #
@@ -647,6 +675,7 @@ cat > Makefile.config <<EOF
 PREFIX=$prefix
 BINDIR=$bindir
 LIBDIR=$libdir
+RELLIBDIR=$rellibdir
 MANDIR=$mandir
 SHAREDIR=$sharedir
 COQDEVDIR=$coqdevdir
@@ -678,6 +707,7 @@ HAS_STANDARD_HEADERS=$has_standard_headers
 INSTALL_COQDEV=$install_coqdev
 LIBMATH=$libmath
 MODEL=$model
+PIC_SUPPORTED=$pic_supported
 SYSTEM=$system
 RESPONSEFILE=$responsefile
 LIBRARY_FLOCQ=$library_Flocq
@@ -741,6 +771,10 @@ ENDIANNESS=
 # SYSTEM=cygwin
 SYSTEM=
 
+# Are we able to produce position-independent code (with the `-fpic` option)?
+#PIC_SUPPORTED=true
+PIC_SUPPORTED=false
+
 # C compiler (for testing only)
 CC=cc
 
@@ -839,6 +873,7 @@ CompCert configuration:
     Hardware model................ $model
     Application binary interface.. $abi
     Endianness.................... $endianness
+    PIC generation supported...... $pic_supported
     OS and development env........ $system
     C compiler.................... $cc $cc_options
     C preprocessor................ $cprepro $cprepro_options
@@ -856,6 +891,15 @@ CompCert configuration:
     Shared config installed in.... $(expandprefix $sharedir)
     Runtime library provided...... $has_runtime_lib
     Library files installed in.... $(expandprefix $libdir)
+EOF
+
+if test "$rellibdir" = "$libdir"; then :; else
+cat <<EOF
+                                   ($rellibdir relative to compcert.ini)
+EOF
+fi
+
+cat <<EOF
     Man pages installed in........ $(expandprefix $mandir)
     Standard headers provided..... $has_standard_headers
     Standard headers installed in. $(expandprefix $libdir)/include
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 995be34d7..391e1ca1a 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -22,6 +22,8 @@ let option_funprototyped = ref true
 let option_fpacked_structs = ref false
 let option_funstructured_switch = ref false
 let option_ffpu = ref true
+let option_fpic = ref false
+let option_fpie = ref Configuration.pic_supported
 let option_ffloatconstprop = ref 2
 let option_ftailcalls = ref true
 let option_fconstprop = ref true
diff --git a/driver/Configuration.ml b/driver/Configuration.ml
index 4b0c116ef..986cff93f 100644
--- a/driver/Configuration.ml
+++ b/driver/Configuration.ml
@@ -142,6 +142,7 @@ let stdlib_path =
   else
     ""
 let asm_supports_cfi = get_bool_config "asm_supports_cfi"
+let pic_supported = get_bool_config "pic_supported"
 
 type response_file_style =
   | Gnu         (* responsefiles in gnu compatible syntax *)
diff --git a/driver/Configuration.mli b/driver/Configuration.mli
index a71da72d6..39f183524 100644
--- a/driver/Configuration.mli
+++ b/driver/Configuration.mli
@@ -59,3 +59,6 @@ val gnu_toolchain: bool
 
 val elf_target: bool
   (** Is the target binary format ELF? *)
+
+val pic_supported: bool
+  (** Are we able to generate PIC and PIE code? *)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 4266e57e0..0052d3288 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -200,6 +200,8 @@ Processing options:
                  single caller [on]
   -fif-conversion Perform if-conversion (generation of conditional moves) [on]
 Code generation options: (use -fno-<opt> to turn off -f<opt>)
+  -fpic / -fPIC  Generate position-independent code [off]
+  -fpie / -fPIE  Generate position-independent executables [on if supported]
   -ffpu          Use FP registers for some integer operations [on]
   -fsmall-data <n>  Set maximal size <n> for allocation in small data area
   -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
@@ -266,6 +268,16 @@ let cmdline_actions =
     if n <= 0 || ((n land (n - 1)) <> 0) then
       error no_loc "requested alignment %d is not a power of 2" n
     in
+  let set_pic_mode () =
+    if Configuration.pic_supported
+    then option_fpic := true
+    else warning no_loc Unnamed
+         "option -fpic not supported on this platform, ignored" in
+  let set_pie_mode () =
+    if Configuration.pic_supported
+    then option_fpie := true
+    else warning no_loc Unnamed
+         "option -fpie not supported on this platform, ignored" in
   [
 (* Getting help *)
   Exact "-help", Unit print_usage_and_exit;
@@ -301,7 +313,15 @@ let cmdline_actions =
   Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); 
   Exact "-falign-functions", Integer(fun n -> check_align n; option_falignfunctions := Some n);
   Exact "-falign-branch-targets", Integer(fun n -> check_align n; option_falignbranchtargets := n);
-  Exact "-falign-cond-branches", Integer(fun n -> check_align n; option_faligncondbranchs := n);] @
+  Exact "-falign-cond-branches", Integer(fun n -> check_align n; option_faligncondbranchs := n);
+  Exact "-fpic", Unit set_pic_mode;
+  Exact "-fPIC", Unit set_pic_mode;
+  Exact "-fno-pic", Unset option_fpic;
+  Exact "-fno-PIC", Unset option_fpic;
+  Exact "-fpie", Unit set_pie_mode;
+  Exact "-fPIE", Unit set_pie_mode;
+  Exact "-fno-pie", Unset option_fpie;
+  Exact "-fno-PIE", Unset option_fpie ] @
       f_opt "common" option_fcommon @
 (* Target processor options *)
   (if Configuration.arch = "arm" then
diff --git a/driver/Linker.ml b/driver/Linker.ml
index d6e1d3843..06b88b73b 100644
--- a/driver/Linker.ml
+++ b/driver/Linker.ml
@@ -39,6 +39,9 @@ let gnu_linker_help =
                  linking
   -nostdlib      Do not use the standard system startup files or
                  libraries when linking
+  -no-pie        Do not produce a position-independent executable
+  -pie           Produce a position-independent executable
+  -shared        Produce a shared library instead of an executable
 |}
 
 let linker_help =
@@ -71,7 +74,10 @@ let linker_actions =
   ] @
   (if Configuration.gnu_toolchain then
     [ Exact "-nodefaultlibs", Self push_linker_arg;
-      Exact "-nostdlib", Self push_linker_arg;]
+      Exact "-nostdlib", Self push_linker_arg;
+      Exact "-pie", Self push_linker_arg;
+      Exact "-no-pie", Self push_linker_arg;
+      Exact "-shared", Self push_linker_arg]
   else []) @
   [ Exact "-s", Self push_linker_arg;
     Exact "-static", Self push_linker_arg;
diff --git a/riscV/Archi.v b/riscV/Archi.v
index ce9357287..52802f9c9 100644
--- a/riscV/Archi.v
+++ b/riscV/Archi.v
@@ -71,7 +71,3 @@ Global Opaque ptr64 big_endian splitlong
               fma_order fma_invalid_mul_is_nan
               float_of_single_preserves_sNaN
               float_conversion_default_nan.
-
-(** Whether to generate position-independent code or not *)
-
-Parameter pic_code: unit -> bool.
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 4e867b678..be00925d9 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -21,6 +21,7 @@ Require Archi.
 Require Import Coqlib Errors.
 Require Import AST Integers Floats Memdata.
 Require Import Op Locations Mach Asm.
+Require SelectOp.
 
 Local Open Scope string_scope.
 Local Open Scope error_monad_scope.
@@ -419,7 +420,7 @@ Definition transl_op
           else Ploadsi rd f :: k)
   | Oaddrsymbol s ofs, nil =>
       do rd <- ireg_of res;
-      OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)
+      OK (if SelectOp.symbol_is_relocatable s && negb (Ptrofs.eq ofs Ptrofs.zero)
           then Ploadsymbol rd s Ptrofs.zero :: addptrofs rd rd ofs k
           else Ploadsymbol rd s ofs :: k)
   | Oaddrstack n, nil =>
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index c6784ee14..ed841616b 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -278,7 +278,7 @@ Opaque Int.eq.
 - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
 - destruct (Float.eq_dec n Float.zero); TailNoLabel.
 - destruct (Float32.eq_dec n Float32.zero); TailNoLabel.
-- destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
+- destruct (SelectOp.symbol_is_relocatable id && negb (Ptrofs.eq ofs Ptrofs.zero)).
 + eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel.
 + TailNoLabel. 
 - apply opimm32_label; intros; exact I.
diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v
index 0f9f2adc2..6e3b260e3 100644
--- a/riscV/Asmgenproof1.v
+++ b/riscV/Asmgenproof1.v
@@ -989,7 +989,7 @@ Opaque Int.eq.
   apply exec_straight_one. simpl; eauto. auto.
   split; intros; Simpl. 
 - (* addrsymbol *)
-  destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
+  destruct (SelectOp.symbol_is_relocatable id && negb (Ptrofs.eq ofs Ptrofs.zero)).
 + set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))).
   exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. 
   intros (rs2 & A & B & C).
diff --git a/riscV/ConstpropOp.vp b/riscV/ConstpropOp.vp
index 75f8a2bb8..ce49245d1 100644
--- a/riscV/ConstpropOp.vp
+++ b/riscV/ConstpropOp.vp
@@ -18,6 +18,7 @@ Require Import Coqlib Compopts.
 Require Import AST Integers Floats.
 Require Import Op Registers.
 Require Import ValueDomain.
+Require SelectOp.
 
 (** * Converting known values to constants *)
 
@@ -298,7 +299,7 @@ Nondetfunction addr_strength_reduction
                 (addr: addressing) (args: list reg) (vl: list aval) :=
   match addr, args, vl with
   | Aindexed n, r1 :: nil, Ptr(Gl symb n1) :: nil =>
-      if Archi.pic_code tt
+      if SelectOp.symbol_is_relocatable symb
       then (addr, args)
       else (Aglobal symb (Ptrofs.add n1 n), nil)
   | Aindexed n, r1 :: nil, Ptr(Stk n1) :: nil =>
diff --git a/riscV/ConstpropOpproof.v b/riscV/ConstpropOpproof.v
index 85a19a0a7..d5355f389 100644
--- a/riscV/ConstpropOpproof.v
+++ b/riscV/ConstpropOpproof.v
@@ -734,7 +734,7 @@ Proof.
   intros until res. unfold addr_strength_reduction.
   destruct (addr_strength_reduction_match addr args vl); simpl;
   intros VL EA; InvApproxRegs; SimplVM; try (inv EA).
-- destruct (Archi.pic_code tt).
+- destruct (SelectOp.symbol_is_relocatable symb).
 + exists (Val.offset_ptr e#r1 n); auto.
 + simpl. rewrite Genv.shift_symbol_address. econstructor; split; eauto. 
   inv H0; simpl; auto.
diff --git a/riscV/SelectOp.vp b/riscV/SelectOp.vp
index 00476b0d1..dfa5fce09 100644
--- a/riscV/SelectOp.vp
+++ b/riscV/SelectOp.vp
@@ -450,10 +450,18 @@ Definition select (ty: typ) (cond: condition) (args: exprlist) (e1 e2: expr) :=
  
 (** ** Recognition of addressing modes for load and store operations *)
 
+(** Some symbols are relocatable (e.g. global symbols in PIC mode)
+    and cannot be used with [Aglobal] addressing mode. *)
+
+Parameter symbol_is_relocatable: ident -> bool.
+
 Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   match e with
   | Eop (Oaddrstack n) Enil => (Ainstack n, Enil)
-  | Eop (Oaddrsymbol id ofs) Enil => if Archi.pic_code tt then (Aindexed Ptrofs.zero, e:::Enil) else (Aglobal id ofs, Enil)
+  | Eop (Oaddrsymbol id ofs) Enil =>
+      if symbol_is_relocatable id
+      then (Aindexed Ptrofs.zero, e:::Enil)
+      else (Aglobal id ofs, Enil)
   | Eop (Oaddimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int n), e1:::Enil)
   | Eop (Oaddlimm n) (e1:::Enil) => (Aindexed (Ptrofs.of_int64 n), e1:::Enil)
   | _ => (Aindexed Ptrofs.zero, e:::Enil)
diff --git a/riscV/SelectOpproof.v b/riscV/SelectOpproof.v
index f5998f28c..391f4ebcb 100644
--- a/riscV/SelectOpproof.v
+++ b/riscV/SelectOpproof.v
@@ -893,7 +893,7 @@ Theorem eval_addressing:
 Proof.
   intros until v. unfold addressing; case (addressing_match a); intros; InvEval.
   - exists (@nil val);  split. eauto with evalexpr. simpl. auto.
-  - destruct (Archi.pic_code tt).
+  - destruct (symbol_is_relocatable id).
   + exists (Vptr b ofs0 :: nil); split.
     constructor. EvalOp. simpl. congruence. constructor. simpl. rewrite Ptrofs.add_zero. congruence.
   + exists (@nil val); split. constructor. simpl; auto.
diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml
index 1144ae26e..fb948b325 100644
--- a/riscV/TargetPrinter.ml
+++ b/riscV/TargetPrinter.ml
@@ -111,7 +111,7 @@ module Target : TARGET =
 (* Generate code to load the address of id + ofs in register r *)
 
     let loadsymbol oc r id ofs =
-      if Archi.pic_code () then begin
+      if SelectOp.symbol_is_relocatable id then begin
         assert (ofs = Integers.Ptrofs.zero);
         fprintf oc "	la	%a, %s\n" ireg r (extern_atom id)
       end else begin
@@ -144,6 +144,13 @@ module Target : TARGET =
         assert (!latest_auipc = Some(id, ofs));
         fprintf oc "%%pcrel_lo(1b)"
 
+(* Emit the target of a call, with a `@plt` suffix in PIC mode. *)
+
+    let symbol_plt oc s =
+      if SelectOp.symbol_is_relocatable s
+      then fprintf oc "%a@plt" symbol s
+      else symbol oc s
+
 (* Printing of instructions *)
     let print_instruction oc = function
       | Pmv(rd, rs) ->
@@ -277,11 +284,11 @@ module Target : TARGET =
       | Pj_l(l) ->
          fprintf oc "	j	%a\n" print_label l
       | Pj_s(s, sg) ->
-         fprintf oc "	jump	%a, x31\n" symbol s
+         fprintf oc "	tail	%a\n" symbol_plt s
       | Pj_r(r, sg) ->
          fprintf oc "	jr	%a\n" ireg r
       | Pjal_s(s, sg) ->
-         fprintf oc "	call	%a\n" symbol s
+         fprintf oc "	call	%a\n" symbol_plt s
       | Pjal_r(r, sg) ->
          fprintf oc "	jalr	%a\n" ireg r
 
@@ -596,7 +603,10 @@ module Target : TARGET =
     let address = if Archi.ptr64 then ".quad" else ".long"
 
     let print_prologue oc =
-      fprintf oc "	.option %s\n" (if Archi.pic_code() then "pic" else "nopic");
+      fprintf oc "	.option %s\n"
+        (if !Clflags.option_fpic || !Clflags.option_fpie
+         then "pic"
+         else "nopic");
       if !Clflags.option_g then begin
         section oc Section_text;
       end
diff --git a/riscV/extractionMachdep.v b/riscV/extractionMachdep.v
index 890735bad..84de6a038 100644
--- a/riscV/extractionMachdep.v
+++ b/riscV/extractionMachdep.v
@@ -16,13 +16,17 @@
 
 (* Additional extraction directives specific to the RISC-V port *)
 
-Require Archi Asm.
+Require Archi Asm SelectOp.
 
 (* Archi *)
 
 Extract Constant Archi.ptr64 => " Configuration.model = ""64"" ".
-Extract Constant Archi.pic_code => "fun () -> false".  (* for the time being *)
+
+(* SelectOp *)
+
+Extract Constant SelectOp.symbol_is_relocatable => "C2C.atom_needs_GOT_access".
 
 (* Asm *)
+
 Extract Constant Asm.low_half => "fun _ _ _ -> assert false".
 Extract Constant Asm.high_half => "fun _ _ _ -> assert false".
diff --git a/test b/test
index 72ca254cc..29085c328 160000
--- a/test
+++ b/test
@@ -1 +1 @@
-Subproject commit 72ca254ccd357849215b596610807bfc3ec2d807
+Subproject commit 29085c328bd6c36ead1cf4319f6486a23f799656
diff --git a/tools/runner.sh b/tools/runner.sh
index 995fc5706..f914c07d8 100755
--- a/tools/runner.sh
+++ b/tools/runner.sh
@@ -181,12 +181,14 @@ case "$target,$os" in
   aarch64,linux)
     case "$1" in
       1) Run_test "$simu_aarch64" "";;
-      2) Run_test "$simu_aarch64" "-Os";;
+      2) Run_test "$simu_aarch64" "-fpic";;
+      3) Run_test "$simu_aarch64" "-Os -fno-pie -no-pie";;
     esac;;
   aarch64,macos)
     case "$1" in
       1) Run_test "" "";;
-      2) Run_test "" "-Os";;
+      2) Run_test "" "-fpic";;
+      3) Run_test "" "-Os";;
     esac;;
   arm,linux)
     case "$1" in
@@ -203,13 +205,20 @@ case "$target,$os" in
   riscv,linux)
     case "$1" in
       1) Run_test "$simu_rv64" "";;
-      2) Run_test "$simu_rv64" "-Os";;
+      2) Run_test "$simu_rv64" "-fpic";;
+      3) Run_test "$simu_rv64" "-Os -fno-pie -no-pie";;
     esac;;
-  x86_32,*|x86_64,*)
+  x86_32,*)
     case "$1" in
       1) Run_test "" "";;
       2) Run_test "" "-Os";;
     esac;;
+  x86_64,*)
+    case "$1" in
+      1) Run_test "" "";;
+      2) Run_test "" "-fpic";;
+      3) Run_test "" "-Os -fno-pie -no-pie";;
+    esac;;
   *)
     Fatal "Unknown configuration \"$target\" - \"$os\""
 esac
diff --git a/x86/ConstpropOp.vp b/x86/ConstpropOp.vp
index ada7ca6be..15c16cf04 100644
--- a/x86/ConstpropOp.vp
+++ b/x86/ConstpropOp.vp
@@ -30,7 +30,7 @@ Definition const_for_result (a: aval) : option operation :=
   | F n => if Compopts.generate_float_constants tt then Some(Ofloatconst n) else None
   | FS n => if Compopts.generate_float_constants tt then Some(Osingleconst n) else None
   | Ptr(Gl id ofs) =>
-      if SelectOp.symbol_is_external id then
+      if SelectOp.symbol_is_relocatable id then
         if Ptrofs.eq ofs Ptrofs.zero then Some (Oindirectsymbol id) else None
       else
         Some (Olea_ptr (Aglobal id ofs))
diff --git a/x86/ConstpropOpproof.v b/x86/ConstpropOpproof.v
index 562495364..0858d78a3 100644
--- a/x86/ConstpropOpproof.v
+++ b/x86/ConstpropOpproof.v
@@ -109,7 +109,7 @@ Proof.
 - (* pointer *)
   destruct p; try discriminate; SimplVM.
   + (* global *)
-    destruct (SelectOp.symbol_is_external id).
+    destruct (SelectOp.symbol_is_relocatable id).
   * revert H2; predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero; intros EQ; inv EQ.
     exists (Genv.symbol_address ge id Ptrofs.zero); auto.
   * inv H2. exists (Genv.symbol_address ge id ofs); split.
diff --git a/x86/SelectOp.vp b/x86/SelectOp.vp
index eb9b203a2..ca4f14937 100644
--- a/x86/SelectOp.vp
+++ b/x86/SelectOp.vp
@@ -48,16 +48,15 @@ Local Open Scope cminorsel_scope.
 
 (** External oracle to determine whether a symbol should be addressed
   through [Oindirectsymbol] or can be addressed via [Oleal Aglobal].
-  This is to accommodate MacOS X's limitations on references to data
-  symbols imported from shared libraries.  It can also help with PIC
-  code under ELF. *)
+  Indirect access is needed for data symbols imported from shared libraries
+  in macOS and Cygwin, and for PIC code in ELF. *)
 
-Parameter symbol_is_external: ident -> bool.
+Parameter symbol_is_relocatable: ident -> bool.
 
 Definition Olea_ptr (a: addressing) := if Archi.ptr64 then Oleal a else Olea a.
 
 Definition addrsymbol (id: ident) (ofs: ptrofs) :=
-  if symbol_is_external id then
+  if symbol_is_relocatable id then
     if Ptrofs.eq ofs Ptrofs.zero
     then Eop (Oindirectsymbol id) Enil
     else Eop (Olea_ptr (Aindexed (Ptrofs.unsigned ofs))) (Eop (Oindirectsymbol id) Enil ::: Enil)
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v
index 1b68b39f0..b73066651 100644
--- a/x86/SelectOpproof.v
+++ b/x86/SelectOpproof.v
@@ -117,7 +117,7 @@ Theorem eval_addrsymbol:
   exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v.
 Proof.
   intros. unfold addrsymbol. exists (Genv.symbol_address ge id ofs); split; auto.
-  destruct (symbol_is_external id).
+  destruct (symbol_is_relocatable id).
   predSpec Ptrofs.eq Ptrofs.eq_spec ofs Ptrofs.zero.
   subst. EvalOp.
   EvalOp. econstructor. EvalOp. simpl; eauto. econstructor.
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml
index 3db1af98d..610be0f5a 100644
--- a/x86/TargetPrinter.ml
+++ b/x86/TargetPrinter.ml
@@ -107,6 +107,7 @@ module type SYSTEM =
       val raw_symbol: out_channel -> string -> unit
       val symbol: out_channel -> P.t -> unit
       val symbol_paren: out_channel -> P.t -> unit
+      val symbol_function: out_channel -> P.t -> unit
       val label: out_channel -> int -> unit
       val name_of_section: section_name -> string
       val stack_alignment: int
@@ -137,6 +138,10 @@ module ELF_System : SYSTEM =
       then fprintf oc "(%s)" s
       else fprintf oc "%s" s
 
+    let symbol_function oc symb =
+      symbol_paren oc symb;
+      if SelectOp.symbol_is_relocatable symb then fprintf oc "@PLT"
+
     let label = elf_label
 
     let name_of_section = function
@@ -206,6 +211,9 @@ module MacOS_System : SYSTEM =
     let symbol_paren = symbol
         (* the leading '_' protects the leading '$' *)
 
+    let symbol_function = symbol
+        (* no need for @PLT even in PIC mode *)
+
     let label oc lbl =
       fprintf oc "L%d" lbl
 
@@ -278,6 +286,8 @@ module Cygwin_System : SYSTEM =
       then fprintf oc "(%a)" raw_symbol s
       else raw_symbol oc s
 
+    let symbol_function = symbol_paren
+
     let label oc lbl =
        fprintf oc "L%d" lbl
 
@@ -723,7 +733,7 @@ module Target(System: SYSTEM):TARGET =
       | Pjmp_l(l) ->
           fprintf oc "	jmp	%a\n" label (transl_label l)
       | Pjmp_s(f, sg) ->
-          fprintf oc "	jmp	%a\n" symbol_paren f
+          fprintf oc "	jmp	%a\n" symbol_function f
       | Pjmp_r(r, sg) ->
           fprintf oc "	jmp	*%a\n" ireg r
       | Pjcc(c, l) ->
@@ -749,7 +759,7 @@ module Target(System: SYSTEM):TARGET =
             fprintf oc "	jmp	*%a(, %a, 4)\n" label l ireg r
           end
       | Pcall_s(f, sg) ->
-          fprintf oc "	call	%a\n" symbol_paren f;
+          fprintf oc "	call	%a\n" symbol_function f;
           if (not Archi.ptr64) && sg.sig_cc.cc_structret then
             fprintf oc "	pushl	%%eax\n"
       | Pcall_r(r, sg) ->
diff --git a/x86/extractionMachdep.v b/x86/extractionMachdep.v
index d1a29c729..72dc0c105 100644
--- a/x86/extractionMachdep.v
+++ b/x86/extractionMachdep.v
@@ -27,8 +27,8 @@ Extract Constant Archi.win64 =>
 
 (* SelectOp *)
 
-Extract Constant SelectOp.symbol_is_external =>
+Extract Constant SelectOp.symbol_is_relocatable =>
   "match Configuration.system with
     | ""macos"" -> C2C.atom_is_external
-    | ""cygwin"" when Archi.ptr64 -> C2C.atom_is_external
-    | _ -> (fun _ -> false)".
+    | ""cygwin"" -> if Archi.ptr64 then C2C.atom_is_external else (fun _ -> false)
+    | _ -> C2C.atom_needs_GOT_access".