Note: This is a public test instance of Red Hat Bugzilla. The data contained within is a snapshot of the live data so any changes you make will not be reflected in the production Bugzilla. Email is disabled so feel free to test any aspect of the site that you want. File any problems you find or give feedback at bugzilla.redhat.com.
Bug 1330098
Summary: | FTBFS: segmentation fault during build | ||
---|---|---|---|
Product: | [Fedora] Fedora | Reporter: | Karsten Hopp <karsten> |
Component: | coq | Assignee: | Alan Dunn <amdunn> |
Status: | CLOSED ERRATA | QA Contact: | Fedora Extras Quality Assurance <extras-qa> |
Severity: | unspecified | Docs Contact: | |
Priority: | medium | ||
Version: | 24 | CC: | amdunn, dan, dwheeler, loganjerry, rjones |
Target Milestone: | --- | ||
Target Release: | --- | ||
Hardware: | ppc64le | ||
OS: | Linux | ||
Whiteboard: | |||
Fixed In Version: | coq-8.6-1.fc25 | Doc Type: | Bug Fix |
Doc Text: | Story Points: | --- | |
Clone Of: | Environment: | ||
Last Closed: | 2017-01-23 05:19:15 UTC | Type: | Bug |
Regression: | --- | Mount Type: | --- |
Documentation: | --- | CRM: | |
Verified Versions: | Category: | --- | |
oVirt Team: | --- | RHEL 7.3 requirements from Atomic Host: | |
Cloudforms Team: | --- | Target Upstream Version: | |
Embargoed: | |||
Bug Depends On: | |||
Bug Blocks: | 1071880 |
Description
Karsten Hopp
2016-04-25 12:10:28 UTC
This is probably related to the new native compilation feature of coq. I'll try to track it down but, if unsuccessful, may have to turn that feature off for ppc64le. Since I already had a ppc64 VM that I used to track down a gap bug, I tried building coq there, but it succeeded. So this bug appears on ppc64le, but not ppc64, unless my VM is somehow significantly different from real hardware. I'll try creating a ppc64le VM next. (Although access to real hardware would be very much appreciated, as these emulated CPUs are really slooooooow.) Oh, when you spoke about VM I thought you already have access to real HW VM. There are OpenPOWER hubs across the world that provide VMs to developers, like the one we manage at Brno Technical University. You can sign up at https://docs.google.com/forms/d/1py0Fg2x9xoQP9yYzOm4DSnJ1buyQBBCWN9Sj_OZuXek/viewform I suspect an ocaml code generation bug on ppc64le. This is not related to the new native compilation feature of coq. The segfault happens with that turned off. The segfault occurs in the function nat_of_int (see plugins/syntax/nat_syntax.ml). On ppc64, which works, that function starts like this: 1d40: 7c 08 02 a6 mflr r0 1d44: f8 01 00 10 std r0,16(r1) 1d48: f8 21 ff 51 stdu r1,-176(r1) 1d4c: f8 81 00 88 std r4,136(r1) 1d50: f8 61 00 80 std r3,128(r1) 1d54: 7c 83 23 78 mr r3,r4 1d58: e9 62 81 08 ld r11,-32504(r2) 1d5c: f8 41 00 28 std r2,40(r1) 1d60: e8 4b 00 08 ld r2,8(r11) 1d64: e9 6b 00 00 ld r11,0(r11) 1d68: 7d 69 03 a6 mtctr r11 1d6c: 4e 80 04 21 bctrl On ppc64le, which segfaults, that function starts like this: 1aa0: 02 00 4c 3c addis r2,r12,2 1aa4: 60 63 42 38 addi r2,r2,25440 1aa8: a6 02 08 7c mflr r0 1aac: 10 00 01 f8 std r0,16(r1) 1ab0: 51 ff 21 f8 stdu r1,-176(r1) 1ab4: 88 00 81 f8 std r4,136(r1) 1ab8: 80 00 61 f8 std r3,128(r1) 1abc: 78 23 83 7c mr r3,r4 1ac0: 08 81 82 e9 ld r12,-32504(r2) 1ac4: 18 00 41 f8 std r2,24(r1) 1ac8: a6 03 89 7d mtctr r12 1acc: 21 04 80 4e bctrl The bctrl instruction is the one that faults, because a bogus address has been loaded into the ctr register. I notice that on ppc64, after loading r11 with -32504(r2), an additional load into r11 of 0(r11) is done, but there is no such corresponding additional load of r12 in the ppc64le code. I also notice that on ppc, the value of r2 appears to come from the caller, where on ppc64le, there are 2 additional instructions at the top of the function that set r2 from the value of r12. Of course, I basically know squat about ppc assembly, so all of that might be utter nonsense. I'm adding Richard Jones to the CC list. Richard, are you aware of any ocaml code generation bugs on ppc64le? Perhaps involving recursive local functions? It wouldn't surprise me if there are still lurking ppc64le codegen bugs. Note that Fedora 24 is still using the out-of-tree code generator written by IBM. New in OCaml 4.03 is an in-tree code generator for POWER written from scratch by Xavier Leroy et al. Therefore I'm not inclined to fix code gen bugs in this version of OCaml unless they are simple/obvious ones. We will get the new code generator in F25. (In reply to Jerry James from comment #4) > Perhaps involving recursive local functions? BTW don't overlook simple stack overflows. These are much more common on POWER because the stack frames are larger. Try doing: ulimit -s 65536 before the build. why-2.36-1.fc25 frama-c-1.13-7.fc25 why3-0.87.3-1.fc25 gappalib-coq-1.3.2-2.fc25 zenon-0.8.2-5.fc25 flocq-2.5.2-4.fc25 coq-8.6-1.fc25 has been submitted as an update to Fedora 25. https://bodhi.fedoraproject.org/updates/FEDORA-2017-033c8000df coq-8.6-1.fc25, flocq-2.5.2-4.fc25, frama-c-1.13-7.fc25, gappalib-coq-1.3.2-2.fc25, why-2.36-1.fc25, why3-0.87.3-1.fc25, zenon-0.8.2-5.fc25 has been pushed to the Fedora 25 testing repository. If problems still persist, please make note of it in this bug report. See https://fedoraproject.org/wiki/QA:Updates_Testing for instructions on how to install test updates. You can provide feedback for this update here: https://bodhi.fedoraproject.org/updates/FEDORA-2017-033c8000df coq-8.6-1.fc25, flocq-2.5.2-4.fc25, frama-c-1.13-7.fc25, gappalib-coq-1.3.2-2.fc25, why-2.36-1.fc25, why3-0.87.3-1.fc25, zenon-0.8.2-5.fc25 has been pushed to the Fedora 25 stable repository. If problems still persist, please make note of it in this bug report. |