Bug #90144 Contribution by Facebook: Detach InnoDB buffer pool before creating core

Description:
Background innformation provided by Facebook:
Abstract:
Core files can be very helpful for debugging production crashes but core dump has been disabled on production due to multiple reasons. One of the reasons is that the core file can be huge due to the huge InnoDB buffer pool within the process. 

This diff introduces a new command line argument '--innodb-dump-core-without-large-mem-buf', when it is set, all the large memory allocation by function os_mem_alloc_large() in InnoDB won't be dumped in the core file by calling Linux API madvise() with argument MADV_DONTDUMP. It can be disabled by '--skip-innodb-dump-core-without-large-mem-buf'. os_mem_alloc_large() is used to allocate large memory chunk for InnoDB buffer pool, file data merge, row log buffer, etc. Buffer pool is the main one. With this feature, the core size will be less than 3GB when the buffer pool size is 60GB so it won't impact production.

- This sys var only take effect when core dump is enabled by setting 'core-file' in my.cnf.
- By default '--innodb-dump-core-without-large-mem-buf' is set in prod to dump smaller cores, but it 
  is not set by default in MTR so that full core file can be dumped.
- This diff also makes sys var core_file readonly.
- There are other bugs that prevent mysqld from dumping cores, e.g. when mysqld switching user from 
  root to a non-root user, etc. Those will be addressed in separated diffs.

Repo: https://github.com/mysql/mysql-server
Patch on top of 5.6.35: https://github.com/mysql/mysql-server/tree/d61eb03ba1b8478d6cb09969ca6c38f330a93178

How to repeat:
See description

Suggested fix:
See contribution code attached

Detach InnoDB buffer pool before creating core 
(*) This code is contributed under the Facebook agreement

Contribution: fb_patch_32.txt (text/plain), 20.07 KiB.

Posted by developer:
 
Fixed as of the upcoming 8.0.14 release, and here's the changelog entry:

"To reduce the size of core files, the innodb_buffer_pool_in_core_file
variable can be disabled to prevent InnoDB buffer pool pages from being
written to core files. 

Thanks to Facebook for the contribution."

MySQL Reference Manual updates. Changes should appear online within 24 hours.

(1) innodb_buffer_pool_in_core_file description
https://dev.mysql.com/doc/refman/8.0/en/innodb-parameters.html

(2) core-file description
https://dev.mysql.com/doc/refman/8.0/en/server-options.html

(3) core_file description
https://dev.mysql.com/doc/refman/8.0/en/server-system-variables.html

(4) core-file-size description
https://dev.mysql.com/doc/refman/8.0/en/mysqld-safe.html

(5) What's New in 8.0
https://dev.mysql.com/doc/refman/8.0/en/mysql-nutshell.html