[Gcl-devel] SGC on MacOS X

[Aurelien Chanudet]

Hi Camm & John,

I tried to investigate this infinite loop issue when building ACL2 with 
SGC enabled. Here are my conclusions. Camm's comments appreciated, as 
always !

The infinite loop is occurring in the memprotect_handler routine which 
gets called in order to handle stratified segfault (in my 
understanding). There's an infinite loop in this memory handler because 
a segfault is occurring from within the handler itself :

Attaching to process 20950.
Reading symbols for shared libraries . done
Reading symbols for shared libraries ........ done
0x00013818 in memprotect_handler (sig=10, code=-1073753784, 
scp=0xbfffd188, addr=0xbfffd148 "") at sgbc.c:1614
1614          sgc_type_map[p+j] = sgc_type_map[p+j] | SGC_TEMP_WRITABLE;
(gdb) p/x (unsigned long) sgc_type_map
$2 = 0x634890
(gdb) call print_regions ()
(gdb) p/x (unsigned long)(sgc_type_map+p+j)
$4 = 0x63c0d8
(gdb) p/x 0x639000+0x1b000
$5 = 0x654000
(gdb) p j
$6 = 0

print_regions () is a function I wrote using Darwin's custom VM 
management routines. It scans the whole address space, and displays 
memory attributes. The output of this routine is (the first column of 
attributes denotes actual protection attributes, the second column 
denotes max protection attributes allowed).

<snip>
  0x634000     0x1000 rwx  rwx  (no zone)
  0x635000     0x1000 rwx  rwx  (no zone)
  0x636000     0x1000 rwx  rwx  (no zone)
  0x637000     0x1000 rwx  rwx  (no zone)
  0x638000     0x1000 rwx  rwx  (no zone)
  0x639000    0x1b000 r x  rwx  (no zone)
  0x654000     0x1000 rwx  rwx  (no zone)
<snip>

It looks as though sgc_type_map[p+j] falls in a non writable area 
([0x639000;0x654000[). As can be seen from the log above, sgc_type_map 
starts at 0x634890. My MAXPAGE has the default value (128*1024).

Turing on DEBUG_MPROTECT in sgbc.c and trying to compile ACL2 yields 
the following output :

<snip>
mprotect(0x62c000,0x8000), sbrk(0)=0xeaae000
prot[893,894,(5),writable]
mprotect(0x634000,0x1000), sbrk(0)=0xeaae000
prot[894,925,(0),not writable]
mprotect(0x635000,0x1f000), sbrk(0)=0xeaae000
prot[925,926,(5),writable]
mprotect(0x654000,0x1000), sbrk(0)=0xeaae000
prot[926,929,(0),not writable]
<snip>
[SGC on]
fault:0x2b8404 [1] (0)  mprotect(0x2b8000,0x1000,0xeaae000)
fault:0x12ac0b8 [4085] (0)  mprotect(0x12ac000,0x1000,0xeaae000)
fault:0x12b2ec8 [4091] (0)  mprotect(0x12b2000,0x1000,0xeaae000)
fault:0x713728 [1116] (0)  mprotect(0x713000,0x1000,0xeaae000)
fault:0x2cec34 [23] (0)  mprotect(0x2ce000,0x1000,0xeaae000)
fault:0x700fd4 [1097] (0)  mprotect(0x700000,0x1000,0xeaae000)
fault:0x7aff000 [30792] (0)  mprotect(0x7aff000,0x1000,0xeaae000)

When running a separate saved_gcl and doing (si::sgc-on t), here is 
what I get :

>(si::sgc-on t)
<snip>
mprotect(0x62c000,0x8000), sbrk(0)=0xa302000
prot[893,894,(5),writable]
mprotect(0x634000,0x1000), sbrk(0)=0xa302000
prot[894,925,(0),not writable]
mprotect(0x635000,0x1f000), sbrk(0)=0xa302000
prot[925,926,(5),writable]
mprotect(0x654000,0x1000), sbrk(0)=0xa302000
prot[926,929,(0),not writable]
mprotect(0x655000,0x3000), sbrk(0)=0xa302000
prot[929,931,(5),writable]
mprotect(0x658000,0x2000), sbrk(0)=0xa302000
prot[931,962,(0),not writable]
<snip>
fault:0x7182f8 [1121] (0)  mprotect(0x718000,0x1000,0xa302000)
fault:0x70b3ac [1108] (0)  mprotect(0x70b000,0x1000,0xa302000)
fault:0x7052d4 [1102] (0)  mprotect(0x705000,0x1000,0xa302000)
fault:0x709c08 [1106] (0)  mprotect(0x709000,0x1000,0xa302000)
fault:0x2c7a98 [16] (0)  mprotect(0x2c7000,0x1000,0xa302000)
T
fault:0x2ce2f8 [23] (0)  mprotect(0x2ce000,0x1000,0xa302000)
fault:0x700cd0 [1097] (0)  mprotect(0x700000,0x1000,0xa302000)
fault:0x2ccc88 [21] (0)  mprotect(0x2cc000,0x1000,0xa302000)
fault:0x12dea5c [4135] (0)  mprotect(0x12de000,0x1000,0xa302000)
fault:0x13806a0 [4297] (0)  mprotect(0x1380000,0x1000,0xa302000)
fault:0x2b8c3c [1] (0)  mprotect(0x2b8000,0x1000,0xa302000)
fault:0x131bf0c [4196] (0)  mprotect(0x131b000,0x1000,0xa302000)
fault:0x13ec008 [4405] (0)  mprotect(0x13ec000,0x1000,0xa302000)

Aurelien