From 62277541b0ea1c687c64df79a543f776b9f58f29 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 9 Sep 2015 09:47:57 +0200 Subject: Added an builtin for the atomic exchange operation. The new builtin __builtin_atomic_exchange(int *a, int *b, int *c) stores *b in *a and sets *c to the old value of *a. --- powerpc/Asmexpand.ml | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 3fffc037..749d5afd 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -64,7 +64,7 @@ let expand_annot_val txt targ args res = Note that lfd and stfd cannot trap on ill-formed floats. *) let offset_in_range ofs = - Int.eq (Asmgen.high_s ofs) Int.zero + Int.eq (Asmgen.high_s ofs) _0 let memcpy_small_arg sz arg tmp = match arg with @@ -276,9 +276,9 @@ let expand_builtin_vstore chunk args = assert false (* Handling of varargs *) -let linkregister_offset = ref Int.zero +let linkregister_offset = ref _0 -let retaddr_offset = ref Int.zero +let retaddr_offset = ref _0 let current_function_stacksize = ref 0l @@ -485,8 +485,19 @@ let expand_builtin_inline name args res = emit (Plwz (res, Cint! retaddr_offset,GPR1)) (* isel *) | "__builtin_isel", [BA (IR a1); BA (IR a2); BA (IR a3)],BR (IR res) -> - emit (Pcmpwi (a1,Cint (Int.zero))); + emit (Pcmpwi (a1,Cint (_0))); emit (Pisel (res,a3,a2,CRbit_2)) + (* atomic operations *) + | "__builtin_atomic_exchange", [BA (IR a1); BA (IR a2); BA (IR a3)],_ -> + emit (Plwz (GPR10,Cint _0,a2)); + emit (Psync); + let lbl = new_label() in + emit (Plabel lbl); + emit (Plwarx (GPR11,GPR0,a1)); + emit (Pstwcx_ (GPR10,GPR0,a1)); + emit (Pbne lbl); + emit (Pisync); + emit (Pstw (GPR11,Cint _0,a3)) (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) @@ -517,7 +528,7 @@ let expand_instruction instr = | Pallocframe(sz, ofs,retofs) -> let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in let sz = camlint_of_coqint sz in - assert (ofs = Int.zero); + assert (ofs = _0); let sz = if variadic then Int32.add sz 96l else sz in let adj = Int32.neg sz in if adj >= -0x8000l then -- cgit From 2dce91b8e2cae0b49c8870df6c727e25aaa180d8 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 9 Sep 2015 15:36:34 +0200 Subject: Add builtin for atomic load. Implement the new __builtin_atomic_load(int *a, int *b); which stores *a in *b. This differs from the atomic_load of the GCC, since the PPC ISA manual states that you must jump before the load again if it fails. --- powerpc/Asmexpand.ml | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 749d5afd..c6bda75c 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -498,6 +498,15 @@ let expand_builtin_inline name args res = emit (Pbne lbl); emit (Pisync); emit (Pstw (GPR11,Cint _0,a3)) + | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ -> + let lbl = new_label() in + emit (Psync); + emit (Plabel lbl); + emit (Plwz (a1,Cint _0,a1)); + emit (Pcmpw (a1,a1)); + emit (Pbne lbl); + emit (Pisync); + emit (Pstw (a1,Cint _0, a2)); (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) -- cgit From 41655f6c8d38270cc50407b0141b443f6ee90100 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 10 Sep 2015 10:20:15 +0200 Subject: Added builtin for atomic compare and exchange. The new __builtin_atomic_compare_exchange(int *ptr,int *exp,int *dsr); writes dsr into ptr if ptr is equal to exp and returns true if ptr is not equal to exp it writes ptr into exp and returns false. --- powerpc/Asmexpand.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index beaef42f..8cd123fe 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -527,7 +527,7 @@ let expand_builtin_inline name args res = and lblneq = new_label () and lblsucc = new_label () in emit (Plwz (GPR10,Cint _0,exp)); - emit (Plwz (GPR11,Cint _0,exp)); + emit (Plwz (GPR11,Cint _0,des)); emit (Psync); emit (Plabel lbls); emit (Plwarx (GPR12,GPR0,dst)); -- cgit From 0de3d126e70dfedfd6f74710da31c4b9636f900a Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 11 Sep 2015 12:05:31 +0200 Subject: Use the gcc version of atomic load. --- powerpc/Asmexpand.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 8cd123fe..5e26e8a6 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -499,12 +499,10 @@ let expand_builtin_inline name args res = emit (Pisync); emit (Pstw (GPR11,Cint _0,a3)) | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ -> - let lbl = new_label() in emit (Psync); - emit (Plabel lbl); emit (Plwz (a1,Cint _0,a1)); emit (Pcmpw (a1,a1)); - emit (Pbne lbl); + emit (Pbne_rel _4); emit (Pisync); emit (Pstw (a1,Cint _0, a2)); | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) -> -- cgit From 9dc0dd73f75875b301c886df40087192d0fad386 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 14 Sep 2015 19:41:39 +0200 Subject: Use fix registers for atomic builtins. In order to avoid clashes during register allocation etc. The builtins now use fixed registers and mark additional registers as destroyed for temporaries. --- powerpc/Asmexpand.ml | 42 +++++++++++++++++++++++++++++++++--------- 1 file changed, 33 insertions(+), 9 deletions(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 5e26e8a6..23c66382 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -506,20 +506,23 @@ let expand_builtin_inline name args res = emit (Pisync); emit (Pstw (a1,Cint _0, a2)); | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) -> - let tmpres = if a1 = res then - GPR11 - else - res in let lbl = new_label() in emit (Psync); emit (Plabel lbl); - emit (Plwarx (tmpres,GPR0,a1)); - emit (Padd (a2,tmpres,a2)); - emit (Pstwcx_ (a2,GPR0,a1)); + emit (Plwarx (res,GPR0,a1)); + emit (Padd (GPR10,res,a2)); + emit (Pstwcx_ (GPR10,GPR0,a1)); + emit (Pbne lbl); + emit (Pisync); + | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR_none -> + let lbl = new_label() in + emit (Psync); + emit (Plabel lbl); + emit (Plwarx (GPR3,GPR0,a1)); + emit (Padd (GPR10,GPR3,a2)); + emit (Pstwcx_ (GPR10,GPR0,a1)); emit (Pbne lbl); emit (Pisync); - if (tmpres <> res) then - emit (Pmr (res,tmpres)) | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR (IR res) -> let lbls = new_label () and lblneq = new_label () @@ -542,6 +545,27 @@ let expand_builtin_inline name args res = emit (Pstw (GPR12,(Cint _0),exp)); emit (Plabel lblsucc); emit (Pmr (res,dst)); + | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR_none -> + let lbls = new_label () + and lblneq = new_label () + and lblsucc = new_label () in + emit (Plwz (GPR10,Cint _0,exp)); + emit (Plwz (GPR11,Cint _0,des)); + emit (Psync); + emit (Plabel lbls); + emit (Plwarx (GPR12,GPR0,dst)); + emit (Pcmpw (GPR12,GPR10)); + emit (Pbne lblneq); + emit (Pstwcx_ (GPR11,GPR0,dst)); + emit (Pbne lbls); + emit (Plabel lblneq); + emit (Pisync); + emit (Pmfcr dst); + emit (Prlwinm (dst,dst,(Z.of_uint 3),_1)); + emit (Pcmpwi (dst,(Cint _0))); + emit (Pbne lblsucc); + emit (Pstw (GPR12,(Cint _0),exp)); + emit (Plabel lblsucc); (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) -- cgit From fb9578680d1cd88650e7e6aa9bf1e1ffd8b32f49 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 15 Sep 2015 12:32:09 +0200 Subject: Removed usage of bne and removed duplicated code for return values of atomics. Instead of introducing a new bne instruction in Asm.v and the TargetPrinter.ml I use the equivalent bf instruction. The duplicated code is due to unused return values of builtins. Now we only emit the additional code for the return value if the return value is used instead of duplicating the whole emiting sequence. --- powerpc/Asmexpand.ml | 58 +++++++++++++++++----------------------------------- 1 file changed, 19 insertions(+), 39 deletions(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 23c66382..098eb49d 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -495,57 +495,32 @@ let expand_builtin_inline name args res = emit (Plabel lbl); emit (Plwarx (GPR11,GPR0,a1)); emit (Pstwcx_ (GPR10,GPR0,a1)); - emit (Pbne lbl); + emit (Pbf (CRbit_2,lbl)); emit (Pisync); emit (Pstw (GPR11,Cint _0,a3)) | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ -> + let lbl = new_label () in emit (Psync); emit (Plwz (a1,Cint _0,a1)); emit (Pcmpw (a1,a1)); - emit (Pbne_rel _4); + emit (Pbf (CRbit_2,lbl)); + emit (Plabel lbl); emit (Pisync); emit (Pstw (a1,Cint _0, a2)); - | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) -> + | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], res -> let lbl = new_label() in + let res = (match res with + | BR (IR res) -> res + | BR_none -> GPR3 + | _ -> raise (Error ("unrecognized builtin " ^ name))) in emit (Psync); emit (Plabel lbl); emit (Plwarx (res,GPR0,a1)); emit (Padd (GPR10,res,a2)); emit (Pstwcx_ (GPR10,GPR0,a1)); - emit (Pbne lbl); - emit (Pisync); - | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR_none -> - let lbl = new_label() in - emit (Psync); - emit (Plabel lbl); - emit (Plwarx (GPR3,GPR0,a1)); - emit (Padd (GPR10,GPR3,a2)); - emit (Pstwcx_ (GPR10,GPR0,a1)); - emit (Pbne lbl); + emit (Pbf (CRbit_2, lbl)); emit (Pisync); - | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR (IR res) -> - let lbls = new_label () - and lblneq = new_label () - and lblsucc = new_label () in - emit (Plwz (GPR10,Cint _0,exp)); - emit (Plwz (GPR11,Cint _0,des)); - emit (Psync); - emit (Plabel lbls); - emit (Plwarx (GPR12,GPR0,dst)); - emit (Pcmpw (GPR12,GPR10)); - emit (Pbne lblneq); - emit (Pstwcx_ (GPR11,GPR0,dst)); - emit (Pbne lbls); - emit (Plabel lblneq); - emit (Pisync); - emit (Pmfcr dst); - emit (Prlwinm (dst,dst,(Z.of_uint 3),_1)); - emit (Pcmpwi (dst,(Cint _0))); - emit (Pbne lblsucc); - emit (Pstw (GPR12,(Cint _0),exp)); - emit (Plabel lblsucc); - emit (Pmr (res,dst)); - | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR_none -> + | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], res -> let lbls = new_label () and lblneq = new_label () and lblsucc = new_label () in @@ -555,17 +530,22 @@ let expand_builtin_inline name args res = emit (Plabel lbls); emit (Plwarx (GPR12,GPR0,dst)); emit (Pcmpw (GPR12,GPR10)); - emit (Pbne lblneq); + emit (Pbf (CRbit_2,lblneq)); emit (Pstwcx_ (GPR11,GPR0,dst)); - emit (Pbne lbls); + emit (Pbf (CRbit_2,lbls)); emit (Plabel lblneq); emit (Pisync); emit (Pmfcr dst); emit (Prlwinm (dst,dst,(Z.of_uint 3),_1)); emit (Pcmpwi (dst,(Cint _0))); - emit (Pbne lblsucc); + emit (Pbf (CRbit_2,lblsucc)); emit (Pstw (GPR12,(Cint _0),exp)); emit (Plabel lblsucc); + (match res with + | BR_none -> () + | BR (IR res) -> + emit (Pmr (res,dst)) + | _ ->raise (Error ("unrecognized builtin " ^ name))) (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) -- cgit From 435dc0e6fe74f0ab06737360e1dc49b42b95f1e4 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 17 Sep 2015 19:20:57 +0200 Subject: Integrated the fix of commit de40fce9c16ced8d23389cbcfc55ef6d99466fe8 for the atomics. --- powerpc/Asmexpand.ml | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 098eb49d..702b6a76 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -507,12 +507,8 @@ let expand_builtin_inline name args res = emit (Plabel lbl); emit (Pisync); emit (Pstw (a1,Cint _0, a2)); - | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], res -> + | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) -> let lbl = new_label() in - let res = (match res with - | BR (IR res) -> res - | BR_none -> GPR3 - | _ -> raise (Error ("unrecognized builtin " ^ name))) in emit (Psync); emit (Plabel lbl); emit (Plwarx (res,GPR0,a1)); @@ -520,7 +516,7 @@ let expand_builtin_inline name args res = emit (Pstwcx_ (GPR10,GPR0,a1)); emit (Pbf (CRbit_2, lbl)); emit (Pisync); - | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], res -> + | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR (IR res) -> let lbls = new_label () and lblneq = new_label () and lblsucc = new_label () in @@ -541,11 +537,7 @@ let expand_builtin_inline name args res = emit (Pbf (CRbit_2,lblsucc)); emit (Pstw (GPR12,(Cint _0),exp)); emit (Plabel lblsucc); - (match res with - | BR_none -> () - | BR (IR res) -> - emit (Pmr (res,dst)) - | _ ->raise (Error ("unrecognized builtin " ^ name))) + emit (Pmr (res,dst)) (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) -- cgit From bc1fbdd0baaab41aa048b3214ec71bb0cc04dfcc Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 21 Sep 2015 16:17:44 +0200 Subject: Applied a few simplification for temporary registers. --- powerpc/Asmexpand.ml | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 702b6a76..9a3804a0 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -493,27 +493,27 @@ let expand_builtin_inline name args res = emit (Psync); let lbl = new_label() in emit (Plabel lbl); - emit (Plwarx (GPR11,GPR0,a1)); + emit (Plwarx (GPR0,GPR0,a1)); emit (Pstwcx_ (GPR10,GPR0,a1)); emit (Pbf (CRbit_2,lbl)); emit (Pisync); - emit (Pstw (GPR11,Cint _0,a3)) + emit (Pstw (GPR0,Cint _0,a3)) | "__builtin_atomic_load", [BA (IR a1); BA (IR a2)],_ -> let lbl = new_label () in emit (Psync); - emit (Plwz (a1,Cint _0,a1)); - emit (Pcmpw (a1,a1)); + emit (Plwz (GPR0,Cint _0,a1)); + emit (Pcmpw (GPR0,GPR0)); emit (Pbf (CRbit_2,lbl)); emit (Plabel lbl); emit (Pisync); - emit (Pstw (a1,Cint _0, a2)); + emit (Pstw (GPR0,Cint _0, a2)) | "__builtin_sync_fetch_and_add", [BA (IR a1); BA(IR a2)], BR (IR res) -> let lbl = new_label() in emit (Psync); emit (Plabel lbl); emit (Plwarx (res,GPR0,a1)); - emit (Padd (GPR10,res,a2)); - emit (Pstwcx_ (GPR10,GPR0,a1)); + emit (Padd (GPR0,res,a2)); + emit (Pstwcx_ (GPR0,GPR0,a1)); emit (Pbf (CRbit_2, lbl)); emit (Pisync); | "__builtin_atomic_compare_exchange", [BA (IR dst); BA(IR exp); BA (IR des)], BR (IR res) -> @@ -524,18 +524,19 @@ let expand_builtin_inline name args res = emit (Plwz (GPR11,Cint _0,des)); emit (Psync); emit (Plabel lbls); - emit (Plwarx (GPR12,GPR0,dst)); - emit (Pcmpw (GPR12,GPR10)); + emit (Plwarx (GPR0,GPR0,dst)); + emit (Pcmpw (GPR0,GPR10)); emit (Pbf (CRbit_2,lblneq)); emit (Pstwcx_ (GPR11,GPR0,dst)); emit (Pbf (CRbit_2,lbls)); emit (Plabel lblneq); + (* Here, CR2 is true if the exchange succeeded, false if it failed *) emit (Pisync); emit (Pmfcr dst); - emit (Prlwinm (dst,dst,(Z.of_uint 3),_1)); - emit (Pcmpwi (dst,(Cint _0))); - emit (Pbf (CRbit_2,lblsucc)); - emit (Pstw (GPR12,(Cint _0),exp)); + emit (Prlwinm (res,res,(Z.of_uint 3),_1)); + (* Update exp with the current value of dst if the exchange failed *) + emit (Pbt (CRbit_2,lblsucc)); + emit (Pstw (GPR0,Cint _0,exp)); emit (Plabel lblsucc); emit (Pmr (res,dst)) (* Catch-all *) -- cgit From 3174d685154a1e0febf305d305fc79422a1adcd3 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Mon, 21 Sep 2015 17:49:22 +0200 Subject: Removed unnecessary move register and use the correct register as base value for the rlwinm. --- powerpc/Asmexpand.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'powerpc/Asmexpand.ml') diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 9a3804a0..23704feb 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -533,12 +533,11 @@ let expand_builtin_inline name args res = (* Here, CR2 is true if the exchange succeeded, false if it failed *) emit (Pisync); emit (Pmfcr dst); - emit (Prlwinm (res,res,(Z.of_uint 3),_1)); + emit (Prlwinm (res,dest,(Z.of_uint 3),_1)); (* Update exp with the current value of dst if the exchange failed *) emit (Pbt (CRbit_2,lblsucc)); emit (Pstw (GPR0,Cint _0,exp)); - emit (Plabel lblsucc); - emit (Pmr (res,dst)) + emit (Plabel lblsucc) (* Catch-all *) | _ -> raise (Error ("unrecognized builtin " ^ name)) -- cgit