4 files changed, 38 insertions, 1 deletions
diff --git a/runtime/include/ccomp_k1c_fixes.h b/runtime/include/ccomp_k1c_fixes.h
index b42323b8..9a2a26c1 100644
--- a/runtime/include/ccomp_k1c_fixes.h
+++ b/runtime/include/ccomp_k1c_fixes.h
@@ -11,6 +11,10 @@
 struct __int128_ccomp { long __int128_ccomp_low; long __int128_ccomp_high; };
 
 #define __int128 struct __int128_ccomp
+
 #define __builtin_k1_acswapd __compcert_acswapd
-extern __int128 __compcert_acswapd(unsigned long long *address, unsigned long long new_value, unsigned long long old_value);
+extern __int128 __compcert_acswapd(void *address, unsigned long long new_value, unsigned long long old_value);
+
+#define __builtin_k1_acswapw __compcert_acswapw
+extern __int128 __compcert_acswapw(void *address, unsigned long long new_value, unsigned long long old_value);
 #endif
diff --git a/runtime/mppa_k1c/vararg.S b/runtime/mppa_k1c/vararg.S
index dbd7b96d..0c96b2ff 100644
--- a/runtime/mppa_k1c/vararg.S
+++ b/runtime/mppa_k1c/vararg.S
@@ -84,3 +84,10 @@ __compcert_acswapd:
 	sq	0[$r0] = $r2r3
 	ret
 	;;
+	.globl __compcert_acswapw
+__compcert_acswapw:
+	acswapw	0[$r1] = $r2r3
+	;;
+	sq	0[$r0] = $r2r3
+	ret
+	;;
diff --git a/test/monniaux/acswap/test_swapd.c b/test/monniaux/acswap/test_swapd.c
new file mode 100644
index 00000000..4841f040
--- /dev/null
+++ b/test/monniaux/acswap/test_swapd.c
@@ -0,0 +1,13 @@
+#include <stdio.h>
+
+int main() {
+  unsigned long long loc=10, next=12, current=11;
+  union {
+    __int128 i128;
+    struct {
+      unsigned long low, high;
+    } i64_2;
+  } ret;
+  ret.i128 = __builtin_k1_acswapd(&loc, next, current);
+  printf("%lx %lx\n", ret.i64_2.low, ret.i64_2.high);
+}
diff --git a/test/monniaux/acswap/test_swapw.c b/test/monniaux/acswap/test_swapw.c
new file mode 100644
index 00000000..906938e0
--- /dev/null
+++ b/test/monniaux/acswap/test_swapw.c
@@ -0,0 +1,13 @@
+#include <stdio.h>
+
+int main() {
+  unsigned loc=11, next=12, current=11;
+  union {
+    __int128 i128;
+    struct {
+      unsigned long low, high;
+    } i64_2;
+  } ret;
+  ret.i128 = __builtin_k1_acswapw(&loc, next, current);
+  printf("%lx %lx\n", ret.i64_2.low, ret.i64_2.high);
+}